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);
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_symbol)
94 else if(type.
id() == ID_typedef_type)
96 else if(type.
id()==ID_vector)
98 else if(type.
id()==ID_custom_unsignedbv ||
99 type.
id()==ID_custom_signedbv ||
100 type.
id()==ID_custom_floatbv ||
101 type.
id()==ID_custom_fixedbv)
103 else if(type.
id()==ID_gcc_attribute_mode)
116 if(underlying_type.id()==ID_c_enum_tag)
121 assert(underlying_type.id()==ID_signedbv ||
122 underlying_type.id()==ID_unsignedbv);
125 if(underlying_type.id()==ID_signedbv ||
126 underlying_type.id()==ID_unsignedbv)
128 bool is_signed=underlying_type.id()==ID_signedbv;
137 else if(
mode==
"__byte__")
142 else if(
mode==
"__HI__")
147 else if(
mode==
"__SI__")
152 else if(
mode==
"__word__")
157 else if(
mode==
"__pointer__")
162 else if(
mode==
"__DI__")
179 else if(
mode==
"__TI__")
184 else if(
mode==
"__V2SI__")
193 else if(
mode==
"__V4SI__")
217 else if(underlying_type.id()==ID_floatbv)
223 else if(
mode==
"__DF__")
225 else if(
mode==
"__TF__")
227 else if(
mode==
"__V2SF__")
229 else if(
mode==
"__V2DF__")
231 else if(
mode==
"__V4SF__")
233 else if(
mode==
"__V4DF__")
243 else if(underlying_type.id()==ID_complex)
250 else if(
mode==
"__DC__")
252 else if(
mode==
"__TC__")
266 <<
"' applied to inappropriate type `" 274 if(type.
get_bool(ID_C_restricted) &&
275 type.
id()!=ID_pointer &&
279 error() <<
"only a pointer can be 'restrict'" <<
eom;
288 static_cast<const exprt &
>(type.
find(ID_size));
298 error() <<
"failed to convert bit vector width to constant" <<
eom;
305 error() <<
"bit vector width invalid" <<
eom;
314 if(type.
id()==ID_custom_unsignedbv)
315 type.
id(ID_unsignedbv);
316 else if(type.
id()==ID_custom_signedbv)
317 type.
id(ID_signedbv);
318 else if(type.
id()==ID_custom_fixedbv)
323 static_cast<const exprt &
>(type.
find(ID_f));
335 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
339 if(f_int<0 || f_int>size_int)
342 error() <<
"fixedbv fraction width invalid" <<
eom;
349 else if(type.
id()==ID_custom_floatbv)
354 static_cast<const exprt &
>(type.
find(ID_f));
366 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
370 if(f_int<1 || f_int+1>=size_int)
373 error() <<
"floatbv fraction width invalid" <<
eom;
393 if(parameters.empty())
400 if(type.
parameters().back().id()==ID_ellipsis)
411 if(param.id()==ID_declaration)
421 std::list<codet> tmp_clean_code;
431 if(identifier.
empty())
446 param.
swap(parameter);
452 if(parameters.size()==1 &&
453 follow(parameters[0].type()).
id()==ID_empty)
471 error() <<
"function must not return array" <<
eom;
478 error() <<
"function must not return function type" <<
eom;
519 error() <<
"failed to convert constant: " 527 error() <<
"array size must not be negative, " 528 "but got " << s <<
eom;
534 else if(tmp_size.
id()==ID_infinity)
538 else if(tmp_size.
id()==ID_symbol &&
558 error() <<
"array size of static symbol `" 580 new_symbol.
name=temp_identifier;
584 new_symbol.
type.
set(ID_C_constant,
true);
585 new_symbol.
value=size;
586 new_symbol.
location=source_location;
600 assignment.
lhs()=symbol_expr;
601 assignment.
rhs()=size;
627 if(subtype.
id()!=ID_signedbv &&
628 subtype.
id()!=ID_unsignedbv &&
629 subtype.
id()!=ID_floatbv &&
630 subtype.
id()!=ID_fixedbv)
633 error() <<
"cannot make a vector of subtype " 644 error() <<
"failed to convert constant: " 652 error() <<
"vector size must be positive, " 653 "but got " << s <<
eom;
667 error() <<
"failed to determine size of vector base type `" 675 error() <<
"type had size 0: `" 684 error() <<
"vector size (" << s
685 <<
") expected to be multiple of base type size (" << sub_size
710 compound_symbol.
type=type;
716 compound_symbol.
base_name=
"#anon-"+typestr;
717 compound_symbol.
name=
"tag-#anon#"+typestr;
718 identifier=compound_symbol.
name;
731 identifier=type.
find(ID_tag).
get(ID_identifier);
734 symbol_tablet::symbolst::const_iterator s_it=
742 type.
set(ID_tag, base_name);
746 compound_symbol.
name=identifier;
748 compound_symbol.
type=type;
754 if(compound_symbol.
type.
id()==ID_struct)
755 compound_symbol.
type.
id(ID_incomplete_struct);
756 else if(compound_symbol.
type.
id()==ID_union)
757 compound_symbol.
type.
id(ID_incomplete_union);
774 if(s_it->second.type.id()==ID_incomplete_struct ||
775 s_it->second.type.id()==ID_incomplete_union)
782 type.
set(ID_tag, base_name);
791 error() <<
"redefinition of body of `" 792 << s_it->second.pretty_name <<
"'" <<
eom;
802 type.
swap(symbol_type);
803 original_qualifiers.
write(type);
812 old_components.swap(components);
815 for(
auto &decl : old_components)
818 assert(decl.id()==ID_declaration);
823 if(declaration.get_is_static_assert())
826 new_component.
id(ID_static_assert);
828 new_component.
operands().swap(declaration.operands());
829 assert(new_component.
operands().size()==2);
830 components.push_back(new_component);
838 for(
const auto &declarator : declaration.declarators())
843 declarator.source_location();
844 new_component.
set(ID_name, declarator.get_base_name());
845 new_component.
set(ID_pretty_name, declarator.get_base_name());
846 new_component.
type()=declaration.full_type(declarator);
851 (new_component.
type().
id()!=ID_array ||
855 error() <<
"incomplete type not permitted here" <<
eom;
859 components.push_back(new_component);
864 unsigned anon_member_counter=0;
867 for(
auto &member : components)
869 if(!member.get_name().empty())
873 member.set_anonymous(
true);
879 std::unordered_set<irep_idt> members;
881 for(struct_union_typet::componentst::iterator
882 it=components.begin();
883 it!=components.end();
886 if(!members.insert(it->get_name()).second)
889 error() <<
"duplicate member '" << it->get_name() <<
'\'' <<
eom;
898 if(type.
id()==ID_struct ||
901 for(struct_union_typet::componentst::iterator
902 it=components.begin();
903 it!=components.end();
906 typet &c_type=it->type();
908 if(c_type.
id()==ID_array &&
912 if(type.
id()==ID_struct && it!=--components.end())
915 error() <<
"flexible struct member must be last member" <<
eom;
930 if(type.
id()==ID_struct)
932 else if(type.
id()==ID_union)
937 for(struct_typet::componentst::iterator
938 it=components.begin();
939 it!=components.end();
942 if(it->type().id()==ID_c_bit_field &&
944 it=components.erase(it);
950 for(struct_union_typet::componentst::iterator
951 it=components.begin();
952 it!=components.end();
955 if(it->id()==ID_static_assert)
957 assert(it->operands().size()==2);
964 if(assertion.is_false())
967 error() <<
"failed _Static_assert" <<
eom;
970 else if(!assertion.is_true())
975 it=components.erase(it);
1017 bool is_packed)
const 1093 std::list<c_enum_typet::c_enum_membert> enum_members;
1122 error() <<
"enum is not a constant";
1132 typet constant_type=
1137 declaration.
type()=constant_type;
1151 enum_members.push_back(member);
1161 bool is_packed=type.
get_bool(ID_C_packed);
1167 std::string anon_identifier=
"#anon_enum";
1169 for(
const auto &member : enum_members)
1171 anon_identifier+=
'$';
1172 anon_identifier+=
id2string(member.get_base_name());
1173 anon_identifier+=
'=';
1174 anon_identifier+=
id2string(member.get_value());
1178 anon_identifier+=
"#packed";
1180 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1191 enum_tag_symbol.
type=type;
1192 enum_tag_symbol.
location=source_location;
1195 enum_tag_symbol.
name=identifier;
1200 for(
const auto &member : enum_members)
1201 body.push_back(member);
1204 typet underlying_type=
1210 symbol_tablet::symbolst::const_iterator s_it=
1216 const symbolt &symbol=s_it->second;
1218 if(symbol.
type.
id()==ID_incomplete_c_enum)
1224 else if(symbol.
type.
id()==ID_c_enum)
1229 if(!base_name.
empty())
1232 error() <<
"redeclaration of enum tag" <<
eom;
1239 error() <<
"use of tag that does not match previous declaration" <<
eom;
1250 type.
id(ID_c_enum_tag);
1252 type.
set(ID_identifier, identifier);
1262 error() <<
"anonymous enum tag without members" <<
eom;
1273 symbol_tablet::symbolst::const_iterator s_it=
1279 const symbolt &symbol=s_it->second;
1281 if(symbol.
type.
id()!=ID_c_enum &&
1282 symbol.
type.
id()!=ID_incomplete_c_enum)
1285 error() <<
"use of tag that does not match previous declaration" <<
eom;
1292 typet new_type(ID_incomplete_c_enum);
1294 new_type.
add(ID_tag)=tag;
1299 enum_tag_symbol.
type=new_type;
1300 enum_tag_symbol.
location=source_location;
1303 enum_tag_symbol.
name=identifier;
1329 error() <<
"failed to convert bit field width" <<
eom;
1336 error() <<
"bit field width is negative" <<
eom;
1346 std::size_t sub_width=0;
1348 if(subtype.
id()==ID_bool)
1353 else if(subtype.
id()==ID_signedbv ||
1354 subtype.
id()==ID_unsignedbv ||
1355 subtype.
id()==ID_c_bool)
1359 else if(subtype.
id()==ID_c_enum_tag)
1364 const typet &c_enum_type=
1367 if(c_enum_type.
id()==ID_incomplete_c_enum)
1370 error() <<
"bit field has incomplete enum type" <<
eom;
1379 error() <<
"bit field with non-integer type: " 1387 error() <<
"bit field (" << i
1388 <<
" bits) larger than type (" << sub_width <<
" bits)" 1401 c_qualifiers.
read(type);
1403 if(!((
const exprt &)type).has_operands())
1415 if(expr.
id()==ID_address_of &&
1428 c_qualifiers.
write(type);
1436 symbol_tablet::symbolst::const_iterator s_it=
1442 error() <<
"type symbol `" << identifier <<
"' not found" 1447 const symbolt &symbol=s_it->second;
1452 error() <<
"expected type symbol" <<
eom;
1461 symbol_tablet::symbolst::const_iterator s_it =
1467 error() <<
"typedef symbol `" << identifier <<
"' not found" <<
eom;
1471 const symbolt &symbol = s_it->second;
1476 error() <<
"expected type symbol for typedef" <<
eom;
1483 bool is_packed = type.
get_bool(ID_C_packed);
1488 c_qualifiers.
write(type);
1491 type.
set(ID_C_packed,
true);
1496 if(symbol.
base_name==
"__CPROVER_rational")
1500 else if(symbol.
base_name==
"__CPROVER_integer")
1508 if(type.
id()==ID_array)
1514 else if(type.
id()==ID_code)
1522 else if(type.
id()==ID_KnR)
bitvector_typet gcc_float128_type()
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.
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 generic typet to a bitvector_typet.
std::vector< irept > subt
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
unsignedbv_typet unsigned_int_type()
const code_typet & to_code_type(const typet &type)
Cast a generic 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
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
id_type_mapt parameter_map
bool is_incomplete() const
irep_idt pretty_name
Language-specific display name.
bitvector_typet double_type()
void set_identifier(const irep_idt &identifier)
unsignedbv_typet size_type()
unsignedbv_typet gcc_unsigned_int128_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
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
typet full_type(const ansi_c_declaratort &) const
signedbv_typet signed_size_type()
const irep_idt & get_identifier() const
#define INVARIANT(CONDITION, REASON)
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)
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
A constant-size array type.
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
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 generic 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
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic 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.
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 generic 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.
virtual void typecheck_symbol_type(symbol_typet &type)
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.
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 of C structs and unions, and C++ classes.
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 generic typet to an array_typet.
Base class for all expressions.
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 generic typet to a struct_union_typet.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
source_locationt & add_source_location()
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const source_locationt & source_location() const
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()
virtual void typecheck_array_type(array_typet &type)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic 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.
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 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()
const typet & return_type() const
const irep_idt & get_identifier() const
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