14 #include <unordered_set> 34 ansi_c_convert_type.
read(type);
35 ansi_c_convert_type.
write(type);
38 if(type.
id()==ID_already_typechecked)
43 bool packed=type.
get_bool(ID_C_packed);
49 c_qualifiers.
write(type);
51 type.
set(ID_C_packed,
true);
55 type.
add(ID_C_typedef, _typedef);
71 if(type.
id()==ID_code)
73 else if(type.
id()==ID_array)
75 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__")
214 else if(underlying_type.id()==ID_floatbv)
220 else if(
mode==
"__DF__")
222 else if(
mode==
"__TF__")
224 else if(
mode==
"__V2SF__")
226 else if(
mode==
"__V2DF__")
228 else if(
mode==
"__V4SF__")
230 else if(
mode==
"__V4DF__")
240 else if(underlying_type.id()==ID_complex)
247 else if(
mode==
"__DC__")
249 else if(
mode==
"__TC__")
263 <<
"' applied to inappropriate type `" 271 if(type.
get_bool(ID_C_restricted) &&
272 type.
id()!=ID_pointer &&
276 error() <<
"only a pointer can be 'restrict'" <<
eom;
285 static_cast<const exprt &
>(type.
find(ID_size));
295 error() <<
"failed to convert bit vector width to constant" <<
eom;
302 error() <<
"bit vector width invalid" <<
eom;
311 if(type.
id()==ID_custom_unsignedbv)
312 type.
id(ID_unsignedbv);
313 else if(type.
id()==ID_custom_signedbv)
314 type.
id(ID_signedbv);
315 else if(type.
id()==ID_custom_fixedbv)
320 static_cast<const exprt &
>(type.
find(ID_f));
332 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
336 if(f_int<0 || f_int>size_int)
339 error() <<
"fixedbv fraction width invalid" <<
eom;
346 else if(type.
id()==ID_custom_floatbv)
351 static_cast<const exprt &
>(type.
find(ID_f));
363 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
367 if(f_int<1 || f_int+1>=size_int)
370 error() <<
"floatbv fraction width invalid" <<
eom;
390 if(parameters.empty())
397 if(type.
parameters().back().id()==ID_ellipsis)
408 if(param.id()==ID_declaration)
418 std::list<codet> tmp_clean_code;
428 if(identifier.
empty())
443 param.
swap(parameter);
449 if(parameters.size()==1 &&
450 follow(parameters[0].type()).
id()==ID_empty)
468 error() <<
"function must not return array" <<
eom;
475 error() <<
"function must not return function type" <<
eom;
516 error() <<
"failed to convert constant: " 524 error() <<
"array size must not be negative, " 525 "but got " << s <<
eom;
531 else if(tmp_size.
id()==ID_infinity)
535 else if(tmp_size.
id()==ID_symbol &&
555 error() <<
"array size of static symbol `" 577 new_symbol.
name=temp_identifier;
581 new_symbol.
type.
set(ID_C_constant,
true);
582 new_symbol.
value=size;
583 new_symbol.
location=source_location;
597 assignment.
lhs()=symbol_expr;
598 assignment.
rhs()=size;
624 if(subtype.
id()!=ID_signedbv &&
625 subtype.
id()!=ID_unsignedbv &&
626 subtype.
id()!=ID_floatbv &&
627 subtype.
id()!=ID_fixedbv)
630 error() <<
"cannot make a vector of subtype " 641 error() <<
"failed to convert constant: " 649 error() <<
"vector size must be positive, " 650 "but got " << s <<
eom;
664 error() <<
"failed to determine size of vector base type `" 672 error() <<
"type had size 0: `" 681 error() <<
"vector size (" << s
682 <<
") expected to be multiple of base type size (" << sub_size
707 compound_symbol.
type=type;
713 compound_symbol.
base_name=
"#anon-"+typestr;
714 compound_symbol.
name=
"tag-#anon#"+typestr;
715 identifier=compound_symbol.
name;
728 identifier=type.
find(ID_tag).
get(ID_identifier);
731 symbol_tablet::symbolst::const_iterator s_it=
739 type.
set(ID_tag, base_name);
743 compound_symbol.
name=identifier;
745 compound_symbol.
type=type;
751 if(compound_symbol.
type.
id()==ID_struct)
752 compound_symbol.
type.
id(ID_incomplete_struct);
753 else if(compound_symbol.
type.
id()==ID_union)
754 compound_symbol.
type.
id(ID_incomplete_union);
771 if(s_it->second.type.id()==ID_incomplete_struct ||
772 s_it->second.type.id()==ID_incomplete_union)
779 type.
set(ID_tag, base_name);
788 error() <<
"redefinition of body of `" 789 << s_it->second.pretty_name <<
"'" <<
eom;
799 type.
swap(symbol_type);
800 original_qualifiers.
write(type);
809 old_components.swap(components);
812 for(
auto &decl : old_components)
815 assert(decl.id()==ID_declaration);
820 if(declaration.get_is_static_assert())
823 new_component.
id(ID_static_assert);
825 new_component.
operands().swap(declaration.operands());
826 assert(new_component.
operands().size()==2);
827 components.push_back(new_component);
835 for(
const auto &declarator : declaration.declarators())
840 declarator.source_location();
841 new_component.
set(ID_name, declarator.get_base_name());
842 new_component.
set(ID_pretty_name, declarator.get_base_name());
843 new_component.
type()=declaration.full_type(declarator);
848 (new_component.
type().
id()!=ID_array ||
852 error() <<
"incomplete type not permitted here" <<
eom;
856 components.push_back(new_component);
861 unsigned anon_member_counter=0;
864 for(
auto &member : components)
866 if(!member.get_name().empty())
870 member.set_anonymous(
true);
876 std::unordered_set<irep_idt> members;
878 for(struct_union_typet::componentst::iterator
879 it=components.begin();
880 it!=components.end();
883 if(!members.insert(it->get_name()).second)
886 error() <<
"duplicate member '" << it->get_name() <<
'\'' <<
eom;
895 if(type.
id()==ID_struct ||
898 for(struct_union_typet::componentst::iterator
899 it=components.begin();
900 it!=components.end();
903 typet &c_type=it->type();
905 if(c_type.
id()==ID_array &&
909 if(type.
id()==ID_struct && it!=--components.end())
912 error() <<
"flexible struct member must be last member" <<
eom;
927 if(type.
id()==ID_struct)
929 else if(type.
id()==ID_union)
934 for(struct_typet::componentst::iterator
935 it=components.begin();
936 it!=components.end();
939 if(it->type().id()==ID_c_bit_field &&
941 it=components.erase(it);
947 for(struct_union_typet::componentst::iterator
948 it=components.begin();
949 it!=components.end();
952 if(it->id()==ID_static_assert)
954 assert(it->operands().size()==2);
961 if(assertion.is_false())
964 error() <<
"failed _Static_assert" <<
eom;
967 else if(!assertion.is_true())
972 it=components.erase(it);
1014 bool is_packed)
const 1090 std::list<c_enum_typet::c_enum_membert> enum_members;
1119 error() <<
"enum is not a constant";
1129 typet constant_type=
1134 declaration.
type()=constant_type;
1148 enum_members.push_back(member);
1158 bool is_packed=type.
get_bool(ID_C_packed);
1164 std::string anon_identifier=
"#anon_enum";
1166 for(
const auto &member : enum_members)
1168 anon_identifier+=
'$';
1169 anon_identifier+=
id2string(member.get_base_name());
1170 anon_identifier+=
'=';
1171 anon_identifier+=
id2string(member.get_value());
1175 anon_identifier+=
"#packed";
1177 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1188 enum_tag_symbol.
type=type;
1189 enum_tag_symbol.
location=source_location;
1192 enum_tag_symbol.
name=identifier;
1197 for(
const auto &member : enum_members)
1198 body.push_back(member);
1201 typet underlying_type=
1207 symbol_tablet::symbolst::const_iterator s_it=
1213 const symbolt &symbol=s_it->second;
1215 if(symbol.
type.
id()==ID_incomplete_c_enum)
1221 else if(symbol.
type.
id()==ID_c_enum)
1226 if(!base_name.
empty())
1229 error() <<
"redeclaration of enum tag" <<
eom;
1236 error() <<
"use of tag that does not match previous declaration" <<
eom;
1247 type.
id(ID_c_enum_tag);
1249 type.
set(ID_identifier, identifier);
1259 error() <<
"anonymous enum tag without members" <<
eom;
1270 symbol_tablet::symbolst::const_iterator s_it=
1276 const symbolt &symbol=s_it->second;
1278 if(symbol.
type.
id()!=ID_c_enum &&
1279 symbol.
type.
id()!=ID_incomplete_c_enum)
1282 error() <<
"use of tag that does not match previous declaration" <<
eom;
1289 typet new_type(ID_incomplete_c_enum);
1291 new_type.
add(ID_tag)=tag;
1296 enum_tag_symbol.
type=new_type;
1297 enum_tag_symbol.
location=source_location;
1300 enum_tag_symbol.
name=identifier;
1326 error() <<
"failed to convert bit field width" <<
eom;
1333 error() <<
"bit field width is negative" <<
eom;
1343 std::size_t sub_width=0;
1345 if(subtype.
id()==ID_bool)
1350 else if(subtype.
id()==ID_signedbv ||
1351 subtype.
id()==ID_unsignedbv ||
1352 subtype.
id()==ID_c_bool)
1356 else if(subtype.
id()==ID_c_enum_tag)
1361 const typet &c_enum_type=
1364 if(c_enum_type.
id()==ID_incomplete_c_enum)
1367 error() <<
"bit field has incomplete enum type" <<
eom;
1376 error() <<
"bit field with non-integer type: " 1384 error() <<
"bit field (" << i
1385 <<
" bits) larger than type (" << sub_width <<
" bits)" 1398 c_qualifiers.
read(type);
1400 if(!((
const exprt &)type).has_operands())
1412 if(expr.
id()==ID_address_of &&
1425 c_qualifiers.
write(type);
1433 symbol_tablet::symbolst::const_iterator s_it=
1439 error() <<
"type symbol `" << identifier <<
"' not found" 1444 const symbolt &symbol=s_it->second;
1449 error() <<
"expected type symbol" <<
eom;
1458 bool is_packed=type.
get_bool(ID_C_packed);
1463 c_qualifiers.
write(type);
1466 type.
set(ID_C_packed,
true);
1472 if(symbol.
base_name==
"__CPROVER_rational")
1476 else if(symbol.
base_name==
"__CPROVER_integer")
1484 if(type.
id()==ID_array)
1490 else if(type.
id()==ID_code)
1498 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.
signed int get_int(const irep_namet &name) const
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
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)
const typet & follow_tag(const union_tag_typet &) const
typet full_type(const ansi_c_declaratort &) const
signedbv_typet signed_size_type()
#define INVARIANT(CONDITION, REASON)
void set_base_name(const irep_idt &name)
symbol_tablet & symbol_table
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.
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.
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()
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)
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