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)
46 bool packed=type.
get_bool(ID_C_packed);
52 c_qualifiers.
write(type);
54 type.
set(ID_C_packed,
true);
58 type.
add(ID_C_typedef, _typedef);
74 if(type.
id()==ID_code)
76 else if(type.
id()==ID_array)
78 else if(type.
id()==ID_pointer)
80 else if(type.
id()==ID_struct ||
83 else if(type.
id()==ID_c_enum)
85 else if(type.
id()==ID_c_enum_tag)
87 else if(type.
id()==ID_c_bit_field)
89 else if(type.
id()==ID_typeof)
91 else if(type.
id()==ID_symbol)
93 else if(type.
id()==ID_vector)
95 else if(type.
id()==ID_custom_unsignedbv ||
96 type.
id()==ID_custom_signedbv ||
97 type.
id()==ID_custom_floatbv ||
98 type.
id()==ID_custom_fixedbv)
100 else if(type.
id()==ID_gcc_attribute_mode)
113 if(underlying_type.id()==ID_c_enum_tag)
118 assert(underlying_type.id()==ID_signedbv ||
119 underlying_type.id()==ID_unsignedbv);
122 if(underlying_type.id()==ID_signedbv ||
123 underlying_type.id()==ID_unsignedbv)
125 bool is_signed=underlying_type.id()==ID_signedbv;
134 else if(
mode==
"__byte__")
139 else if(
mode==
"__HI__")
144 else if(
mode==
"__SI__")
149 else if(
mode==
"__word__")
154 else if(
mode==
"__pointer__")
159 else if(
mode==
"__DI__")
176 else if(
mode==
"__TI__")
181 else if(
mode==
"__V2SI__")
190 else if(
mode==
"__V4SI__")
210 symbol_tablet::symbolst::iterator entry=
214 entry->second.type.subtype()=
result;
219 else if(underlying_type.id()==ID_floatbv)
225 else if(
mode==
"__DF__")
227 else if(
mode==
"__TF__")
229 else if(
mode==
"__V2SF__")
231 else if(
mode==
"__V2DF__")
233 else if(
mode==
"__V4SF__")
235 else if(
mode==
"__V4DF__")
245 else if(underlying_type.id()==ID_complex)
252 else if(
mode==
"__DC__")
254 else if(
mode==
"__TC__")
268 <<
"' applied to inappropriate type `" 276 if(type.
get_bool(ID_C_restricted) &&
277 type.
id()!=ID_pointer &&
281 error() <<
"only a pointer can be 'restrict'" <<
eom;
290 static_cast<const exprt &
>(type.
find(ID_size));
300 error() <<
"failed to convert bit vector width to constant" <<
eom;
307 error() <<
"bit vector width invalid" <<
eom;
316 if(type.
id()==ID_custom_unsignedbv)
317 type.
id(ID_unsignedbv);
318 else if(type.
id()==ID_custom_signedbv)
319 type.
id(ID_signedbv);
320 else if(type.
id()==ID_custom_fixedbv)
325 static_cast<const exprt &
>(type.
find(ID_f));
337 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
341 if(f_int<0 || f_int>size_int)
344 error() <<
"fixedbv fraction width invalid" <<
eom;
351 else if(type.
id()==ID_custom_floatbv)
356 static_cast<const exprt &
>(type.
find(ID_f));
368 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
372 if(f_int<1 || f_int+1>=size_int)
375 error() <<
"floatbv fraction width invalid" <<
eom;
395 if(parameters.empty())
402 if(type.
parameters().back().id()==ID_ellipsis)
413 if(param.id()==ID_declaration)
423 std::list<codet> tmp_clean_code;
433 if(identifier.
empty())
448 param.
swap(parameter);
454 if(parameters.size()==1 &&
455 follow(parameters[0].type()).
id()==ID_empty)
473 error() <<
"function must not return array" <<
eom;
480 error() <<
"function must not return function type" <<
eom;
521 error() <<
"failed to convert constant: " 529 error() <<
"array size must not be negative, " 530 "but got " << s <<
eom;
536 else if(tmp_size.
id()==ID_infinity)
540 else if(tmp_size.
id()==ID_symbol &&
560 error() <<
"array size of static symbol `" 573 suffix=
"$array_size"+std::to_string(count);
582 new_symbol.
name=temp_identifier;
586 new_symbol.
type.
set(ID_C_constant,
true);
589 new_symbol.
value=size;
590 new_symbol.
location=source_location;
603 assignment.
lhs()=symbol_expr;
604 assignment.
rhs()=size;
630 if(subtype.
id()!=ID_signedbv &&
631 subtype.
id()!=ID_unsignedbv &&
632 subtype.
id()!=ID_floatbv &&
633 subtype.
id()!=ID_fixedbv)
636 error() <<
"cannot make a vector of subtype " 647 error() <<
"failed to convert constant: " 655 error() <<
"vector size must be positive, " 656 "but got " << s <<
eom;
670 error() <<
"failed to determine size of vector base type `" 678 error() <<
"type had size 0: `" 687 error() <<
"vector size (" << s
688 <<
") expected to be multiple of base type size (" << sub_size
713 compound_symbol.
type=type;
719 compound_symbol.
base_name=
"#anon-"+typestr;
720 compound_symbol.
name=
"tag-#anon#"+typestr;
721 identifier=compound_symbol.
name;
734 identifier=type.
find(ID_tag).
get(ID_identifier);
737 symbol_tablet::symbolst::iterator s_it=
745 type.
set(ID_tag, base_name);
749 compound_symbol.
name=identifier;
751 compound_symbol.
type=type;
757 if(compound_symbol.
type.
id()==ID_struct)
758 compound_symbol.
type.
id(ID_incomplete_struct);
759 else if(compound_symbol.
type.
id()==ID_union)
760 compound_symbol.
type.
id(ID_incomplete_union);
777 if(s_it->second.type.id()==ID_incomplete_struct ||
778 s_it->second.type.id()==ID_incomplete_union)
785 type.
set(ID_tag, base_name);
788 s_it->second.type.swap(type);
794 error() <<
"redefinition of body of `" 795 << s_it->second.pretty_name <<
"'" <<
eom;
806 type.
swap(symbol_type);
807 original_qualifiers.
write(type);
816 old_components.swap(components);
819 for(
auto &decl : old_components)
822 assert(decl.id()==ID_declaration);
827 if(declaration.get_is_static_assert())
830 new_component.
id(ID_static_assert);
832 new_component.
operands().swap(declaration.operands());
833 assert(new_component.
operands().size()==2);
834 components.push_back(new_component);
842 for(
const auto &declarator : declaration.declarators())
847 declarator.source_location();
848 new_component.
set(ID_name, declarator.get_base_name());
849 new_component.
set(ID_pretty_name, declarator.get_base_name());
850 new_component.
type()=declaration.full_type(declarator);
855 (new_component.
type().
id()!=ID_array ||
859 error() <<
"incomplete type not permitted here" <<
eom;
863 components.push_back(new_component);
868 unsigned anon_member_counter=0;
871 for(
auto &member : components)
873 if(!member.get_name().empty())
876 member.set_name(
"$anon"+std::to_string(anon_member_counter++));
877 member.set_anonymous(
true);
883 std::unordered_set<irep_idt, irep_id_hash> members;
885 for(struct_union_typet::componentst::iterator
886 it=components.begin();
887 it!=components.end();
890 if(!members.insert(it->get_name()).second)
893 error() <<
"duplicate member '" << it->get_name() <<
'\'' <<
eom;
902 if(type.
id()==ID_struct ||
905 for(struct_union_typet::componentst::iterator
906 it=components.begin();
907 it!=components.end();
910 typet &c_type=it->type();
912 if(c_type.
id()==ID_array &&
916 if(type.
id()==ID_struct && it!=--components.end())
919 error() <<
"flexible struct member must be last member" <<
eom;
934 if(type.
id()==ID_struct)
936 else if(type.
id()==ID_union)
941 for(struct_typet::componentst::iterator
942 it=components.begin();
943 it!=components.end();
946 if(it->type().id()==ID_c_bit_field &&
948 it=components.erase(it);
954 for(struct_union_typet::componentst::iterator
955 it=components.begin();
956 it!=components.end();
959 if(it->id()==ID_static_assert)
961 assert(it->operands().size()==2);
968 if(assertion.is_false())
971 error() <<
"failed _Static_assert" <<
eom;
974 else if(!assertion.is_true())
979 it=components.erase(it);
1021 bool is_packed)
const 1095 mp_integer value=0, min_value=0, max_value=0;
1097 std::list<c_enum_typet::c_enum_membert> enum_members;
1126 error() <<
"enum is not a constant";
1136 typet constant_type=
1141 declaration.
type()=constant_type;
1155 enum_members.push_back(member);
1165 bool is_packed=type.
get_bool(ID_C_packed);
1171 std::string anon_identifier=
"#anon_enum";
1173 for(
const auto &member : enum_members)
1175 anon_identifier+=
'$';
1176 anon_identifier+=
id2string(member.get_base_name());
1177 anon_identifier+=
'=';
1178 anon_identifier+=
id2string(member.get_value());
1182 anon_identifier+=
"#packed";
1184 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1195 enum_tag_symbol.
type=type;
1196 enum_tag_symbol.
location=source_location;
1199 enum_tag_symbol.
name=identifier;
1204 for(
const auto &member : enum_members)
1205 body.push_back(member);
1208 typet underlying_type=
1214 symbol_tablet::symbolst::iterator s_it=
1222 if(symbol.
type.
id()==ID_incomplete_c_enum)
1228 else if(symbol.
type.
id()==ID_c_enum)
1233 if(!base_name.
empty())
1236 error() <<
"redeclaration of enum tag" <<
eom;
1243 error() <<
"use of tag that does not match previous declaration" <<
eom;
1254 type.
id(ID_c_enum_tag);
1256 type.
set(ID_identifier, identifier);
1266 error() <<
"anonymous enum tag without members" <<
eom;
1277 symbol_tablet::symbolst::const_iterator s_it=
1283 const symbolt &symbol=s_it->second;
1285 if(symbol.
type.
id()!=ID_c_enum &&
1286 symbol.
type.
id()!=ID_incomplete_c_enum)
1289 error() <<
"use of tag that does not match previous declaration" <<
eom;
1296 typet new_type(ID_incomplete_c_enum);
1298 new_type.
add(ID_tag)=tag;
1303 enum_tag_symbol.
type=new_type;
1304 enum_tag_symbol.
location=source_location;
1307 enum_tag_symbol.
name=identifier;
1333 error() <<
"failed to convert bit field width" <<
eom;
1340 error() <<
"bit field width is negative" <<
eom;
1350 std::size_t sub_width=0;
1352 if(subtype.
id()==ID_bool)
1357 else if(subtype.
id()==ID_signedbv ||
1358 subtype.
id()==ID_unsignedbv ||
1359 subtype.
id()==ID_c_bool)
1363 else if(subtype.
id()==ID_c_enum_tag)
1368 const typet &c_enum_type=
1371 if(c_enum_type.
id()==ID_incomplete_c_enum)
1374 error() <<
"bit field has incomplete enum type" <<
eom;
1383 error() <<
"bit field with non-integer type: " 1391 error() <<
"bit field (" << i
1392 <<
" bits) larger than type (" << sub_width <<
" bits)" 1405 c_qualifiers.
read(type);
1407 if(!((
const exprt &)type).has_operands())
1419 if(expr.
id()==ID_address_of &&
1432 c_qualifiers.
write(type);
1440 symbol_tablet::symbolst::const_iterator s_it=
1446 error() <<
"type symbol `" << identifier <<
"' not found" 1451 const symbolt &symbol=s_it->second;
1456 error() <<
"expected type symbol" <<
eom;
1465 bool is_packed=type.
get_bool(ID_C_packed);
1470 c_qualifiers.
write(type);
1473 type.
set(ID_C_packed,
true);
1479 if(symbol.
base_name==
"__CPROVER_rational")
1483 else if(symbol.
base_name==
"__CPROVER_integer")
1491 if(type.
id()==ID_array)
1493 type.
id(ID_pointer);
1495 type.
remove(ID_C_constant);
1497 else if(type.
id()==ID_code)
1503 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.
irep_idt name
The unique identifier.
bool is_signed(const typet &t)
Convenience function – is the type signed?
const typet & follow(const typet &src) const
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
std::vector< irept > subt
virtual void make_constant(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
unsignedbv_typet unsigned_int_type()
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
signed int get_int(const irep_namet &name) const
Unbounded, signed rational numbers.
std::vector< componentt > componentst
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
id_type_mapt parameter_map
bool is_incomplete() const
void set_identifier(const irep_idt &identifier)
irep_idt pretty_name
Language-specific display name.
bitvector_typet double_type()
void set_identifier(const irep_idt &identifier)
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
virtual void typecheck_symbol_type(typet &type)
void set_identifier(const irep_idt &identifier)
virtual std::string to_string(const exprt &expr)
virtual void typecheck_compound_type(struct_union_typet &type)
typet full_type(const ansi_c_declaratort &) const
signedbv_typet signed_size_type()
void set_base_name(const irep_idt &name)
symbol_tablet & symbol_table
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const typet & follow_tag(const union_tag_typet &src) const
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
void read(const typet &src)
const irep_idt & id() const
exprt c_sizeof(const typet &src, const namespacet &ns)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
irep_idt get_base_name() const
void add_padding(struct_typet &type, const namespacet &ns)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
void set_value(const irep_idt &value)
ANSI-C Language Type Checking.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
virtual void typecheck_c_enum_type(typet &type)
A reference into the symbol table.
ANSI-C Language Type Checking.
bitvector_typet float_type()
A declaration of a local variable.
const source_locationt & find_source_location() const
void make_already_typechecked(typet &dest)
source_locationt source_location
unsigned long_long_int_width
A constant-size array type.
virtual void make_index_type(exprt &expr)
void write(typet &src) const
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
irep_idt get_name() const
#define PRECONDITION(CONDITION)
signedbv_typet signed_long_int_type()
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 c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
bitvector_typet index_type()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
std::list< codet > clean_code
ANSI-C Language Conversion.
std::size_t get_width() const
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual void typecheck_custom_type(typet &type)
virtual void adjust_function_parameter(typet &type) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const source_locationt & source_location() const
signedbv_typet signed_short_int_type()
Unbounded, signed integers.
Complex numbers made of pair of given subtype.
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()
unsignedbv_typet gcc_unsigned_int128_type()
virtual void typecheck_vector_type(vector_typet &type)
Base type of C structs and unions, and C++ classes.
bitvector_typet gcc_float128_type()
virtual void typecheck_compound_body(struct_union_typet &type)
unsignedbv_typet unsigned_short_int_type()
Base class for all expressions.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
source_locationt & add_source_location()
const source_locationt & source_location() const
virtual void make_constant_index(exprt &expr)
ANSI-CC Language Type Checking.
irept & add(const irep_namet &name)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_identifier(const irep_idt &identifier)
source_locationt & add_source_location()
unsignedbv_typet unsigned_long_long_int_type()
virtual void typecheck_array_type(array_typet &type)
static void add_rounding_mode(exprt &)
Expression to hold a symbol (variable)
virtual void typecheck_type(typet &type)
signedbv_typet signed_int_type()
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
unsignedbv_typet unsigned_char_type()
void remove(const irep_namet &name)
const typet & subtype() const
unsignedbv_typet unsigned_long_int_type()
signedbv_typet gcc_signed_int128_type()
signedbv_typet signed_long_long_int_type()
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
const irept & find(const irep_namet &name) const
signedbv_typet signed_char_type()
const typet & return_type() const
const irep_idt & get_identifier() const
void set_base_name(const irep_idt &base_name)
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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
const ansi_c_declaratort & declarator() const