Go to the documentation of this file.
14 #include <unordered_set>
37 ansi_c_convert_type.
read(type);
38 ansi_c_convert_type.
write(type);
41 if(type.
id()==ID_already_typechecked)
49 bool packed=type.
get_bool(ID_C_packed);
53 type = already_typechecked.
get_type();
55 c_qualifiers.
write(type);
57 type.
set(ID_C_packed,
true);
61 type.
add(ID_C_typedef, _typedef);
77 if(type.
id()==ID_code)
79 else if(type.
id()==ID_array)
81 else if(type.
id()==ID_pointer)
87 else if(type.
id()==ID_struct ||
90 else if(type.
id()==ID_c_enum)
92 else if(type.
id()==ID_c_enum_tag)
94 else if(type.
id()==ID_c_bit_field)
96 else if(type.
id()==ID_typeof)
98 else if(type.
id() == ID_typedef_type)
100 else if(type.
id() == ID_struct_tag ||
101 type.
id() == ID_union_tag)
105 else if(type.
id()==ID_vector)
109 else if(type.
id() == ID_frontend_vector)
113 else if(type.
id()==ID_custom_unsignedbv ||
114 type.
id()==ID_custom_signedbv ||
115 type.
id()==ID_custom_floatbv ||
116 type.
id()==ID_custom_fixedbv)
118 else if(type.
id()==ID_gcc_attribute_mode)
131 if(underlying_type.
id()==ID_c_enum_tag)
136 assert(underlying_type.
id()==ID_signedbv ||
137 underlying_type.
id()==ID_unsignedbv);
140 if(underlying_type.
id()==ID_signedbv ||
141 underlying_type.
id()==ID_unsignedbv)
147 if(gcc_attr_mode ==
"__QI__")
154 else if(gcc_attr_mode ==
"__byte__")
161 else if(gcc_attr_mode ==
"__HI__")
168 else if(gcc_attr_mode ==
"__SI__")
175 else if(gcc_attr_mode ==
"__word__")
182 else if(gcc_attr_mode ==
"__pointer__")
189 else if(gcc_attr_mode ==
"__DI__")
208 else if(gcc_attr_mode ==
"__TI__")
215 else if(gcc_attr_mode ==
"__V2SI__")
226 else if(gcc_attr_mode ==
"__V4SI__")
252 else if(underlying_type.
id()==ID_floatbv)
256 if(gcc_attr_mode ==
"__SF__")
258 else if(gcc_attr_mode ==
"__DF__")
260 else if(gcc_attr_mode ==
"__TF__")
262 else if(gcc_attr_mode ==
"__V2SF__")
264 else if(gcc_attr_mode ==
"__V2DF__")
266 else if(gcc_attr_mode ==
"__V4SF__")
268 else if(gcc_attr_mode ==
"__V4DF__")
278 else if(underlying_type.
id()==ID_complex)
283 if(gcc_attr_mode ==
"__SC__")
285 else if(gcc_attr_mode ==
"__DC__")
287 else if(gcc_attr_mode ==
"__TC__")
300 error() <<
"attribute mode '" << gcc_attr_mode
301 <<
"' applied to inappropriate type '" <<
to_string(type) <<
"'"
309 if(type.
get_bool(ID_C_restricted) &&
310 type.
id()!=ID_pointer &&
314 error() <<
"only a pointer can be 'restrict'" <<
eom;
323 static_cast<const exprt &
>(type.
find(ID_size));
333 error() <<
"failed to convert bit vector width to constant" <<
eom;
340 error() <<
"bit vector width invalid" <<
eom;
349 if(type.
id()==ID_custom_unsignedbv)
350 type.
id(ID_unsignedbv);
351 else if(type.
id()==ID_custom_signedbv)
352 type.
id(ID_signedbv);
353 else if(type.
id()==ID_custom_fixedbv)
358 static_cast<const exprt &
>(type.
find(ID_f));
371 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
375 if(f_int<0 || f_int>size_int)
378 error() <<
"fixedbv fraction width invalid" <<
eom;
385 else if(type.
id()==ID_custom_floatbv)
390 static_cast<const exprt &
>(type.
find(ID_f));
403 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
407 if(f_int<1 || f_int+1>=size_int)
410 error() <<
"floatbv fraction width invalid" <<
eom;
430 if(parameters.empty())
437 if(type.
parameters().back().id()==ID_ellipsis)
448 if(param.id()==ID_declaration)
458 std::list<codet> tmp_clean_code;
468 if(identifier.
empty())
483 param.
swap(parameter);
489 if(parameters.size() == 1 && parameters[0].type().id() == ID_empty)
504 if(decl_return_type.
id() == ID_array)
507 error() <<
"function must not return array" <<
eom;
511 if(decl_return_type.
id() == ID_code)
514 error() <<
"function must not return function type" <<
eom;
539 (followed_subtype.
id() == ID_struct || followed_subtype.
id() == ID_union) &&
544 error() <<
"array has incomplete element type" <<
eom;
553 error() <<
"array of function element type" <<
eom;
577 error() <<
"failed to convert constant: "
585 error() <<
"array size must not be negative, "
586 "but got " << s <<
eom;
592 else if(tmp_size.
id()==ID_infinity)
596 else if(tmp_size.
id()==ID_symbol &&
617 <<
"' is not constant" <<
eom;
625 size_source_location,
628 new_symbol.
type.
set(ID_C_constant,
true);
638 assignment.
lhs()=symbol_expr;
639 assignment.
rhs() = new_symbol.
value;
668 if(subtype.
id()!=ID_signedbv &&
669 subtype.
id()!=ID_unsignedbv &&
670 subtype.
id()!=ID_floatbv &&
671 subtype.
id()!=ID_fixedbv)
674 error() <<
"cannot make a vector of subtype "
685 error() <<
"failed to convert constant: "
693 error() <<
"vector size must be positive, "
694 "but got " << s <<
eom;
701 if(!sub_size_expr_opt.has_value())
704 error() <<
"failed to determine size of vector base type '"
709 simplify(sub_size_expr_opt.value(), *
this);
711 const auto sub_size = numeric_cast<mp_integer>(sub_size_expr_opt.value());
713 if(!sub_size.has_value())
716 error() <<
"failed to determine size of vector base type '"
729 if(s % *sub_size != 0)
732 error() <<
"vector size (" << s
733 <<
") expected to be multiple of base type size (" << *sub_size
762 remove_qualifiers.
write(type);
764 bool is_packed = type.
get_bool(ID_C_packed);
775 compound_symbol.
type=type;
780 std::string typestr =
type2name(compound_symbol.
type, *
this);
781 compound_symbol.
base_name =
"#anon#" + typestr;
782 compound_symbol.
name=
"tag-#anon#"+typestr;
783 identifier=compound_symbol.
name;
796 identifier=type.
find(ID_tag).
get(ID_identifier);
799 symbol_tablet::symbolst::const_iterator s_it=
807 type.
set(ID_tag, base_name);
811 compound_symbol.
name=identifier;
813 compound_symbol.
type=type;
836 s_it->second.type.id() == type.
id() &&
844 type.
set(ID_tag, base_name);
853 error() <<
"redefinition of body of '" << s_it->second.pretty_name
862 if(type.
id() == ID_union)
864 else if(type.
id() == ID_struct)
872 original_qualifiers.
write(type);
875 type.
set(ID_C_packed,
true);
886 old_components.swap(components);
889 for(
auto &decl : old_components)
892 assert(decl.id()==ID_declaration);
900 new_component.
id(ID_static_assert);
903 assert(new_component.
operands().size()==2);
904 components.push_back(new_component);
912 for(
const auto &declarator : declaration.
declarators())
915 declarator.get_base_name(), declaration.
full_type(declarator));
921 : declarator.source_location();
929 (new_component.
type().
id()!=ID_array ||
933 error() <<
"incomplete type not permitted here" <<
eom;
937 components.push_back(new_component);
942 unsigned anon_member_counter=0;
945 for(
auto &member : components)
947 if(!member.get_name().empty())
951 member.set_anonymous(
true);
957 std::unordered_set<irep_idt> members;
959 for(
const auto &c : components)
961 if(!members.insert(c.get_name()).second)
964 error() <<
"duplicate member '" << c.get_name() <<
'\'' <<
eom;
973 if(type.
id()==ID_struct ||
976 for(struct_union_typet::componentst::iterator
977 it=components.begin();
978 it!=components.end();
981 typet &c_type=it->type();
983 if(c_type.
id()==ID_array &&
987 if(type.
id()==ID_struct && it!=--components.
end())
990 error() <<
"flexible struct member must be last member" <<
eom;
1005 if(type.
id()==ID_struct)
1007 else if(type.
id()==ID_union)
1012 for(struct_typet::componentst::iterator
1013 it=components.begin();
1014 it!=components.end();
1017 if(it->type().id()==ID_c_bit_field &&
1019 it=components.erase(it);
1025 for(struct_union_typet::componentst::iterator
1026 it=components.begin();
1027 it!=components.end();
1030 if(it->id()==ID_static_assert)
1041 error() <<
"failed _Static_assert" <<
eom;
1049 it=components.erase(it);
1091 bool is_packed)
const
1163 const bool have_underlying_type =
1166 if(have_underlying_type)
1170 const typet &underlying_type =
1171 static_cast<const typet &
>(type.
find(ID_enum_underlying_type));
1175 std::ostringstream msg;
1176 msg << source_location <<
": non-integral type '"
1177 << underlying_type.
get(ID_C_c_type)
1178 <<
"' is an invalid underlying type";
1185 mp_integer value=0, min_value=0, max_value=0;
1187 std::list<c_enum_typet::c_enum_membert> enum_members;
1211 tmp_v.
id() == ID_constant &&
1218 error() <<
"enum is not a constant" <<
eom;
1228 typet constant_type;
1230 if(have_underlying_type)
1232 constant_type = type.
find_type(ID_enum_underlying_type);
1235 if(value < tmp.smallest() || value > tmp.largest())
1237 std::ostringstream msg;
1240 <<
": enumerator value is not representable in the underlying type '"
1241 << constant_type.
get(ID_C_c_type) <<
"'";
1252 declaration.
type()=constant_type;
1268 enum_members.push_back(member);
1278 bool is_packed=type.
get_bool(ID_C_packed);
1283 if(have_underlying_type)
1294 std::size_t width = underlying_type.
get_width();
1295 for(
auto &member : enum_members)
1307 std::string anon_identifier=
"#anon_enum";
1309 for(
const auto &member : enum_members)
1311 anon_identifier+=
'$';
1312 anon_identifier+=
id2string(member.get_base_name());
1313 anon_identifier+=
'=';
1314 anon_identifier+=
id2string(member.get_value());
1318 anon_identifier+=
"#packed";
1320 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1331 enum_tag_symbol.
type=type;
1332 enum_tag_symbol.
location=source_location;
1335 enum_tag_symbol.
name=identifier;
1340 for(
const auto &member : enum_members)
1341 body.push_back(member);
1346 symbol_tablet::symbolst::const_iterator s_it=
1352 const symbolt &symbol=s_it->second;
1354 if(symbol.
type.
id() != ID_c_enum)
1357 error() <<
"use of tag that does not match previous declaration" <<
eom;
1372 if(!base_name.
empty())
1375 error() <<
"redeclaration of enum tag" <<
eom;
1387 type.
id(ID_c_enum_tag);
1389 type.
set(ID_identifier, identifier);
1399 error() <<
"anonymous enum tag without members" <<
eom;
1406 warning() <<
"ignoring specification of underlying type for enum" <<
eom;
1416 symbol_tablet::symbolst::const_iterator s_it=
1422 const symbolt &symbol=s_it->second;
1424 if(symbol.
type.
id() != ID_c_enum)
1427 error() <<
"use of tag that does not match previous declaration" <<
eom;
1435 new_type.
add(ID_tag)=tag;
1441 enum_tag_symbol.
type=new_type;
1442 enum_tag_symbol.
location=source_location;
1445 enum_tag_symbol.
name=identifier;
1471 error() <<
"failed to convert bit field width" <<
eom;
1478 error() <<
"bit field width is negative" <<
eom;
1482 type.
set_width(numeric_cast_v<std::size_t>(i));
1488 std::size_t sub_width=0;
1490 if(subtype.
id()==ID_bool)
1495 else if(subtype.
id()==ID_signedbv ||
1496 subtype.
id()==ID_unsignedbv ||
1497 subtype.
id()==ID_c_bool)
1501 else if(subtype.
id()==ID_c_enum_tag)
1506 const auto &c_enum_type =
1509 if(c_enum_type.is_incomplete())
1512 error() <<
"bit field has incomplete enum type" <<
eom;
1521 error() <<
"bit field with non-integer type: "
1529 error() <<
"bit field (" << i
1530 <<
" bits) larger than type (" << sub_width <<
" bits)"
1543 c_qualifiers.
read(type);
1545 const auto &as_expr = (
const exprt &)type;
1547 if(!as_expr.has_operands())
1559 if(expr.
id()==ID_address_of &&
1569 c_qualifiers.
write(type);
1576 symbol_tablet::symbolst::const_iterator s_it =
1582 error() <<
"typedef symbol '" << identifier <<
"' not found" <<
eom;
1586 const symbolt &symbol = s_it->second;
1591 error() <<
"expected type symbol for typedef" <<
eom;
1598 bool is_packed = type.
get_bool(ID_C_packed);
1603 c_qualifiers.
write(type);
1606 type.
set(ID_C_packed,
true);
1623 if(type.
id()==ID_array)
1629 else if(type.
id()==ID_code)
1637 else if(type.
id()==ID_KnR)
virtual void read(const typet &src) override
const irep_idt & get_identifier() const
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
void set_identifier(const irep_idt &identifier)
const typet & subtype() const
virtual void typecheck_vector_type(typet &type)
bool is_incomplete() const
const declaratorst & declarators() const
void set_value(const irep_idt &value)
bool is_incomplete() const
enum types may be incomplete
virtual void typecheck_array_type(array_typet &type)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
signedbv_typet signed_long_long_int_type()
signedbv_typet signed_char_type()
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Unbounded, signed rational numbers.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
std::vector< parametert > parameterst
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
ANSI-C Language Type Checking.
Fresh auxiliary symbol creation.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
ANSI-C Language Conversion.
void typecheck_declaration(ansi_c_declarationt &)
virtual std::string to_string(const exprt &expr)
Base type for structs and unions.
typet type
Type of symbol.
virtual void write(typet &type)
static void add_rounding_mode(exprt &)
bool is_signed(const typet &t)
Convenience function – is the type signed?
irept & add(const irep_namet &name)
const mp_integer string2integer(const std::string &n, unsigned base)
const irept & find(const irep_namet &name) const
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
A codet representing the declaration of a local variable.
Unbounded, signed integers (mathematical integers, not bitvectors)
bitvector_typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
Base class for all expressions.
std::vector< componentt > componentst
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Complex numbers made of pair of given subtype.
Thrown when we can't handle something in an input source file.
void make_incomplete()
enum types may be incomplete
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_type(typet &type)
void make_incomplete()
A struct/union may be incomplete.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
unsignedbv_typet unsigned_char_type()
bool is_true() const
Return whether the expression is a constant representing true.
const irep_idt & get_identifier() const
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
bitvector_typet index_type()
const ansi_c_declaratort & declarator() const
floatbv_typet gcc_float128_type()
bool get_is_static_assert() const
A union tag type, i.e., union_typet with an identifier.
unsignedbv_typet unsigned_short_int_type()
bool is_false() const
Return whether the expression is a constant representing false.
std::list< codet > clean_code
already_typechecked_typet & to_already_typechecked_type(typet &type)
irep_idt get_name() const
irep_idt pretty_name
Language-specific display name.
virtual void make_constant(exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
const exprt & size() const
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
mstreamt & result() const
signedbv_typet signed_int_type()
void add_padding(struct_typet &type, const namespacet &ns)
irep_idt get_base_name() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
source_locationt source_location
signedbv_typet gcc_signed_int128_type()
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
virtual bool is_complete_type(const typet &type) const
void set_pretty_name(const irep_idt &name)
signedbv_typet signed_short_int_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
virtual void write(typet &src) const override
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
floatbv_typet float_type()
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
signedbv_typet signed_size_type()
bool simplify(exprt &expr, const namespacet &ns)
std::size_t long_long_int_width
void set_identifier(const irep_idt &identifier)
symbol_tablet & symbol_table
mp_integer alignment(const typet &type, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
unsignedbv_typet unsigned_int_type()
virtual void make_constant_index(exprt &expr)
const irep_idt & id() const
virtual void typecheck_typedef_type(typet &type)
void remove(const irep_namet &name)
virtual void typecheck_typeof_type(typet &type)
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() const
source_locationt & add_source_location()
const constant_exprt & size() const
void set_width(std::size_t width)
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
id_type_mapt parameter_map
void set_base_name(const irep_idt &name)
floatbv_typet double_type()
virtual void typecheck_expr(exprt &expr)
std::size_t get_width() const
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
C enum tag type, i.e., c_enum_typet with an identifier.
std::string::const_iterator end() const
void set_base_name(const irep_idt &base_name)
Base class of fixed-width bit-vector types.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool is_constant() const
Return whether the expression is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
typet full_type(const ansi_c_declaratort &) const
unsignedbv_typet gcc_unsigned_int128_type()
virtual void typecheck_custom_type(typet &type)
std::size_t short_int_width
signedbv_typet signed_long_int_type()
static void make_already_typechecked(typet &type)
const typet & return_type() const
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
virtual void read(const typet &type)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
typet & add_type(const irep_namet &name)
virtual void typecheck_c_enum_type(typet &type)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
virtual void typecheck_compound_type(struct_union_typet &type)
source_locationt & add_source_location()
Semantic type conversion.
unsignedbv_typet size_type()
const typet & find_type(const irep_namet &name) const
A codet representing an assignment in the program.
virtual void typecheck_code_type(code_typet &type)
mstreamt & warning() const
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
irep_idt name
The unique identifier.
bool is_transparent_union
virtual void typecheck_compound_body(struct_union_typet &type)
std::size_t long_int_width
virtual void make_index_type(exprt &expr)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
virtual void adjust_function_parameter(typet &type) const
ANSI-C Language Type Checking.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)