14 #include <unordered_set> 35 ansi_c_convert_type.
read(type);
36 ansi_c_convert_type.
write(type);
39 if(type.
id()==ID_already_typechecked)
44 bool packed=type.
get_bool(ID_C_packed);
50 c_qualifiers.
write(type);
52 type.
set(ID_C_packed,
true);
55 if(_typedef.is_not_nil())
56 type.
add(ID_C_typedef, _typedef);
72 if(type.
id()==ID_code)
74 else if(type.
id()==ID_array)
76 else if(type.
id()==ID_pointer)
81 else if(type.
id()==ID_struct ||
84 else if(type.
id()==ID_c_enum)
86 else if(type.
id()==ID_c_enum_tag)
88 else if(type.
id()==ID_c_bit_field)
90 else if(type.
id()==ID_typeof)
92 else if(type.
id() == ID_typedef_type)
94 else if(type.
id() == ID_struct_tag ||
95 type.
id() == ID_union_tag)
99 else if(type.
id()==ID_vector)
101 else if(type.
id()==ID_custom_unsignedbv ||
102 type.
id()==ID_custom_signedbv ||
103 type.
id()==ID_custom_floatbv ||
104 type.
id()==ID_custom_fixedbv)
106 else if(type.
id()==ID_gcc_attribute_mode)
119 if(underlying_type.id()==ID_c_enum_tag)
124 assert(underlying_type.id()==ID_signedbv ||
125 underlying_type.id()==ID_unsignedbv);
128 if(underlying_type.id()==ID_signedbv ||
129 underlying_type.id()==ID_unsignedbv)
131 bool is_signed=underlying_type.id()==ID_signedbv;
135 if(gcc_attr_mode ==
"__QI__")
142 else if(gcc_attr_mode ==
"__byte__")
149 else if(gcc_attr_mode ==
"__HI__")
156 else if(gcc_attr_mode ==
"__SI__")
163 else if(gcc_attr_mode ==
"__word__")
170 else if(gcc_attr_mode ==
"__pointer__")
177 else if(gcc_attr_mode ==
"__DI__")
196 else if(gcc_attr_mode ==
"__TI__")
203 else if(gcc_attr_mode ==
"__V2SI__")
214 else if(gcc_attr_mode ==
"__V4SI__")
240 else if(underlying_type.id()==ID_floatbv)
244 if(gcc_attr_mode ==
"__SF__")
246 else if(gcc_attr_mode ==
"__DF__")
248 else if(gcc_attr_mode ==
"__TF__")
250 else if(gcc_attr_mode ==
"__V2SF__")
252 else if(gcc_attr_mode ==
"__V2DF__")
254 else if(gcc_attr_mode ==
"__V4SF__")
256 else if(gcc_attr_mode ==
"__V4DF__")
266 else if(underlying_type.id()==ID_complex)
271 if(gcc_attr_mode ==
"__SC__")
273 else if(gcc_attr_mode ==
"__DC__")
275 else if(gcc_attr_mode ==
"__TC__")
288 error() <<
"attribute mode `" << gcc_attr_mode
289 <<
"' applied to inappropriate type `" <<
to_string(type) <<
"'" 297 if(type.
get_bool(ID_C_restricted) &&
298 type.
id()!=ID_pointer &&
302 error() <<
"only a pointer can be 'restrict'" <<
eom;
311 static_cast<const exprt &>(type.
find(ID_size));
321 error() <<
"failed to convert bit vector width to constant" <<
eom;
328 error() <<
"bit vector width invalid" <<
eom;
337 if(type.
id()==ID_custom_unsignedbv)
338 type.
id(ID_unsignedbv);
339 else if(type.
id()==ID_custom_signedbv)
340 type.
id(ID_signedbv);
341 else if(type.
id()==ID_custom_fixedbv)
346 static_cast<const exprt &>(type.
find(ID_f));
359 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
363 if(f_int<0 || f_int>size_int)
366 error() <<
"fixedbv fraction width invalid" <<
eom;
373 else if(type.
id()==ID_custom_floatbv)
378 static_cast<const exprt &>(type.
find(ID_f));
391 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
395 if(f_int<1 || f_int+1>=size_int)
398 error() <<
"floatbv fraction width invalid" <<
eom;
418 if(parameters.empty())
425 if(type.
parameters().back().id()==ID_ellipsis)
436 if(param.id()==ID_declaration)
446 std::list<codet> tmp_clean_code;
456 if(identifier.
empty())
471 param.
swap(parameter);
477 if(parameters.size()==1 &&
478 follow(parameters[0].type()).
id()==ID_empty)
493 if(decl_return_type.id() == ID_array)
496 error() <<
"function must not return array" <<
eom;
500 if(decl_return_type.id() == ID_code)
503 error() <<
"function must not return function type" <<
eom;
531 error() <<
"array has incomplete element type" <<
eom;
540 error() <<
"array of function element type" <<
eom;
564 error() <<
"failed to convert constant: " 572 error() <<
"array size must not be negative, " 573 "but got " << s <<
eom;
579 else if(tmp_size.
id()==ID_infinity)
583 else if(tmp_size.
id()==ID_symbol &&
603 error() <<
"array size of static symbol `" 624 new_symbol.
name=temp_identifier;
628 new_symbol.
type.
set(ID_C_constant,
true);
629 new_symbol.
value=size;
630 new_symbol.
location = size_source_location;
644 assignment.
lhs()=symbol_expr;
645 assignment.
rhs()=size;
671 if(subtype.
id()!=ID_signedbv &&
672 subtype.
id()!=ID_unsignedbv &&
673 subtype.
id()!=ID_floatbv &&
674 subtype.
id()!=ID_fixedbv)
677 error() <<
"cannot make a vector of subtype " 688 error() <<
"failed to convert constant: " 696 error() <<
"vector size must be positive, " 697 "but got " << s <<
eom;
711 error() <<
"failed to determine size of vector base type `" 719 error() <<
"type had size 0: `" 728 error() <<
"vector size (" << s
729 <<
") expected to be multiple of base type size (" << sub_size
754 remove_qualifiers.
write(type);
764 compound_symbol.
type=type;
770 compound_symbol.
base_name=
"#anon-"+typestr;
771 compound_symbol.
name=
"tag-#anon#"+typestr;
772 identifier=compound_symbol.
name;
785 identifier=type.
find(ID_tag).
get(ID_identifier);
788 symbol_tablet::symbolst::const_iterator s_it=
796 type.
set(ID_tag, base_name);
800 compound_symbol.
name=identifier;
802 compound_symbol.
type=type;
808 if(compound_symbol.
type.
id()==ID_struct)
809 compound_symbol.
type.
id(ID_incomplete_struct);
810 else if(compound_symbol.
type.
id()==ID_union)
811 compound_symbol.
type.
id(ID_incomplete_union);
828 if(s_it->second.type.id()==ID_incomplete_struct ||
829 s_it->second.type.id()==ID_incomplete_union)
836 type.
set(ID_tag, base_name);
845 error() <<
"redefinition of body of `" 846 << s_it->second.pretty_name <<
"'" <<
eom;
854 if(type.
id() == ID_union || type.
id() == ID_incomplete_union)
856 else if(type.
id() == ID_struct || type.
id() == ID_incomplete_struct)
864 original_qualifiers.
write(type);
873 old_components.swap(components);
876 for(
auto &decl : old_components)
879 assert(decl.id()==ID_declaration);
884 if(declaration.get_is_static_assert())
887 new_component.
id(ID_static_assert);
889 new_component.
operands().swap(declaration.operands());
890 assert(new_component.
operands().size()==2);
891 components.push_back(new_component);
899 for(
const auto &declarator : declaration.declarators())
902 declarator.get_base_name(), declaration.full_type(declarator));
907 declarator.get_name().empty() ? declaration.source_location()
908 : declarator.source_location();
910 new_component.add_source_location() = source_location;
911 new_component.set_pretty_name(declarator.get_base_name());
916 (new_component.type().id()!=ID_array ||
920 error() <<
"incomplete type not permitted here" <<
eom;
924 components.push_back(new_component);
929 unsigned anon_member_counter=0;
932 for(
auto &member : components)
934 if(!member.get_name().empty())
938 member.set_anonymous(
true);
944 std::unordered_set<irep_idt> members;
946 for(
const auto &c : components)
948 if(!members.insert(c.get_name()).second)
951 error() <<
"duplicate member '" << c.get_name() <<
'\'' <<
eom;
960 if(type.
id()==ID_struct ||
963 for(struct_union_typet::componentst::iterator
964 it=components.begin();
965 it!=components.end();
968 typet &c_type=it->type();
970 if(c_type.
id()==ID_array &&
974 if(type.
id()==ID_struct && it!=--components.
end())
977 error() <<
"flexible struct member must be last member" <<
eom;
992 if(type.
id()==ID_struct)
994 else if(type.
id()==ID_union)
999 for(struct_typet::componentst::iterator
1000 it=components.begin();
1001 it!=components.end();
1004 if(it->type().id()==ID_c_bit_field &&
1006 it=components.erase(it);
1012 for(struct_union_typet::componentst::iterator
1013 it=components.begin();
1014 it!=components.end();
1017 if(it->id()==ID_static_assert)
1019 assert(it->operands().size()==2);
1026 if(assertion.is_false())
1029 error() <<
"failed _Static_assert" <<
eom;
1032 else if(!assertion.is_true())
1037 it=components.erase(it);
1079 bool is_packed)
const 1139 exprt &as_expr=static_cast<exprt &>(static_cast<irept &>(type));
1155 std::list<c_enum_typet::c_enum_membert> enum_members;
1184 error() <<
"enum is not a constant";
1194 typet constant_type=
1199 declaration.
type()=constant_type;
1213 enum_members.push_back(member);
1223 bool is_packed=type.
get_bool(ID_C_packed);
1229 std::string anon_identifier=
"#anon_enum";
1231 for(
const auto &member : enum_members)
1233 anon_identifier+=
'$';
1234 anon_identifier+=
id2string(member.get_base_name());
1235 anon_identifier+=
'=';
1236 anon_identifier+=
id2string(member.get_value());
1240 anon_identifier+=
"#packed";
1242 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1253 enum_tag_symbol.
type=type;
1254 enum_tag_symbol.
location=source_location;
1257 enum_tag_symbol.
name=identifier;
1262 for(
const auto &member : enum_members)
1263 body.push_back(member);
1266 typet underlying_type=
1272 symbol_tablet::symbolst::const_iterator s_it=
1278 const symbolt &symbol=s_it->second;
1280 if(symbol.
type.
id()==ID_incomplete_c_enum)
1286 else if(symbol.
type.
id()==ID_c_enum)
1291 if(!base_name.
empty())
1294 error() <<
"redeclaration of enum tag" <<
eom;
1301 error() <<
"use of tag that does not match previous declaration" <<
eom;
1312 type.
id(ID_c_enum_tag);
1314 type.
set(ID_identifier, identifier);
1324 error() <<
"anonymous enum tag without members" <<
eom;
1335 symbol_tablet::symbolst::const_iterator s_it=
1341 const symbolt &symbol=s_it->second;
1343 if(symbol.
type.
id()!=ID_c_enum &&
1344 symbol.
type.
id()!=ID_incomplete_c_enum)
1347 error() <<
"use of tag that does not match previous declaration" <<
eom;
1354 typet new_type(ID_incomplete_c_enum);
1356 new_type.
add(ID_tag)=tag;
1361 enum_tag_symbol.
type=new_type;
1362 enum_tag_symbol.
location=source_location;
1365 enum_tag_symbol.
name=identifier;
1383 exprt &width_expr=static_cast<exprt &>(type.
add(ID_size));
1391 error() <<
"failed to convert bit field width" <<
eom;
1398 error() <<
"bit field width is negative" <<
eom;
1402 type.
set_width(numeric_cast_v<std::size_t>(i));
1408 std::size_t sub_width=0;
1410 if(subtype.
id()==ID_bool)
1415 else if(subtype.
id()==ID_signedbv ||
1416 subtype.
id()==ID_unsignedbv ||
1417 subtype.
id()==ID_c_bool)
1421 else if(subtype.
id()==ID_c_enum_tag)
1426 const typet &c_enum_type=
1429 if(c_enum_type.
id()==ID_incomplete_c_enum)
1432 error() <<
"bit field has incomplete enum type" <<
eom;
1441 error() <<
"bit field with non-integer type: " 1449 error() <<
"bit field (" << i
1450 <<
" bits) larger than type (" << sub_width <<
" bits)" 1463 c_qualifiers.
read(type);
1465 if(!((
const exprt &)type).has_operands())
1467 typet t=static_cast<const typet &>(type.
find(ID_type_arg));
1477 if(expr.
id()==ID_address_of &&
1490 c_qualifiers.
write(type);
1497 symbol_tablet::symbolst::const_iterator s_it =
1503 error() <<
"typedef symbol `" << identifier <<
"' not found" <<
eom;
1507 const symbolt &symbol = s_it->second;
1512 error() <<
"expected type symbol for typedef" <<
eom;
1519 bool is_packed = type.
get_bool(ID_C_packed);
1524 c_qualifiers.
write(type);
1527 type.
set(ID_C_packed,
true);
1544 if(type.
id()==ID_array)
1550 else if(type.
id()==ID_code)
1558 else if(type.
id()==ID_KnR)
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
virtual void typecheck_typeof_type(typet &type)
The type of an expression, extends irept.
irep_idt name
The unique identifier.
signedbv_typet gcc_signed_int128_type()
exprt size_of_expr(const typet &type, const namespacet &ns)
bool is_signed(const typet &t)
Convenience function – is the type signed?
struct configt::ansi_ct ansi_c
virtual bool is_complete_type(const typet &type) const
void typecheck_declaration(ansi_c_declarationt &)
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::vector< irept > subt
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
unsignedbv_typet unsigned_int_type()
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Unbounded, signed rational numbers.
std::vector< componentt > componentst
bool is_false() const
Return whether the expression is a constant representing false.
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
A union tag type, i.e., union_typet with an identifier.
const componentst & components() const
id_type_mapt parameter_map
bool is_incomplete() const
A struct tag type, i.e., struct_typet with an identifier.
bool is_true() const
Return whether the expression is a constant representing true.
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
void set_identifier(const irep_idt &identifier)
unsignedbv_typet size_type()
unsignedbv_typet gcc_unsigned_int128_type()
bool get_bool(const irep_namet &name) const
void set_identifier(const irep_idt &identifier)
virtual std::string to_string(const exprt &expr)
virtual void typecheck_compound_type(struct_union_typet &type)
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
typet full_type(const ansi_c_declaratort &) const
signedbv_typet signed_size_type()
const irep_idt & get_identifier() const
void set_base_name(const irep_idt &name)
symbol_tablet & symbol_table
virtual void typecheck_typedef_type(typet &type)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
const irep_idt & id() const
irep_idt get_base_name() const
std::size_t long_long_int_width
void add_padding(struct_typet &type, const namespacet &ns)
void set_value(const irep_idt &value)
ANSI-C Language Type Checking.
virtual void typecheck_c_enum_type(typet &type)
ANSI-C Language Type Checking.
A codet representing the declaration of a local variable.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
void make_already_typechecked(typet &dest)
source_locationt source_location
virtual void make_index_type(exprt &expr)
mp_integer alignment(const typet &type, const namespacet &ns)
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
const exprt & size() const
bool is_transparent_union
irep_idt get_name() const
virtual void read(const typet &src) override
#define PRECONDITION(CONDITION)
signedbv_typet signed_long_int_type()
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const exprt & size() const
virtual void typecheck_expr(exprt &expr)
Base class for tree-like data structures with sharing.
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::list< codet > clean_code
ANSI-C Language Conversion.
bool is_constant() const
Return whether the expression is a constant.
std::size_t get_width() const
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
virtual void typecheck_custom_type(typet &type)
virtual void adjust_function_parameter(typet &type) const
const source_locationt & source_location() const
signedbv_typet signed_short_int_type()
Unbounded, signed integers (mathematical integers, not bitvectors)
Complex numbers made of pair of given subtype.
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
floatbv_typet float_type()
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
virtual void typecheck_code_type(code_typet &type)
void read(const typet &type)
message_handlert & get_message_handler()
virtual void typecheck_vector_type(vector_typet &type)
Base type for structs and unions.
mstreamt & result() const
virtual void typecheck_compound_body(struct_union_typet &type)
unsignedbv_typet unsigned_short_int_type()
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
floatbv_typet double_type()
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
source_locationt & add_source_location()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
void set_identifier(const irep_idt &identifier)
virtual void write(typet &src) const override
source_locationt & add_source_location()
unsignedbv_typet unsigned_long_long_int_type()
std::string::const_iterator end() const
virtual void typecheck_array_type(array_typet &type)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
static void add_rounding_mode(exprt &)
Expression to hold a symbol (variable)
virtual void typecheck_type(typet &type)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
floatbv_typet gcc_float128_type()
signedbv_typet signed_int_type()
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
unsignedbv_typet unsigned_char_type()
void remove(const irep_namet &name)
const typet & subtype() const
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_long_long_int_type()
std::size_t long_int_width
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
std::size_t get_size_t(const irep_namet &name) const
const irept & find(const irep_namet &name) const
signedbv_typet signed_char_type()
C enum tag type, i.e., c_enum_typet with an identifier.
const typet & return_type() const
A codet representing an assignment in the program.
void set_base_name(const irep_idt &base_name)
std::size_t short_int_width
void set(const irep_namet &name, const irep_idt &value)
bool simplify(exprt &expr, const namespacet &ns)
void set_width(std::size_t width)
const ansi_c_declaratort & declarator() const