32#include <unordered_set>
39 ansi_c_convert_type.
write(type);
42 if(type.
id()==ID_already_typechecked)
50 bool packed=type.
get_bool(ID_C_packed);
54 type = already_typechecked.
get_type();
56 c_qualifiers.
write(type);
58 type.
set(ID_C_packed,
true);
62 type.
add(ID_C_typedef, _typedef);
78 if(type.
id()==ID_code)
80 else if(type.
id()==ID_array)
82 else if(type.
id()==ID_pointer)
88 else if(type.
id()==ID_struct ||
91 else if(type.
id()==ID_c_enum)
93 else if(type.
id()==ID_c_enum_tag)
95 else if(type.
id()==ID_c_bit_field)
97 else if(type.
id() == ID_typeof || type.
id() == ID_c_typeof_unqual)
99 else if(type.
id() == ID_typedef_type)
101 else if(type.
id() == ID_struct_tag ||
102 type.
id() == ID_union_tag)
106 else if(type.
id()==ID_vector)
110 else if(type.
id() == ID_frontend_vector)
114 else if(type.
id()==ID_custom_unsignedbv ||
115 type.
id()==ID_custom_signedbv ||
116 type.
id()==ID_custom_floatbv ||
117 type.
id()==ID_custom_fixedbv)
119 else if(type.
id() == ID_c_signed_bitint || type.
id() == ID_c_unsigned_bitint)
123 else if(type.
id()==ID_gcc_attribute_mode)
136 if(underlying_type.
id()==ID_c_enum_tag)
142 underlying_type.
id() == ID_signedbv ||
143 underlying_type.
id() == ID_unsignedbv,
144 "underlying type must be bitvector");
147 if(underlying_type.
id()==ID_signedbv ||
148 underlying_type.
id()==ID_unsignedbv)
154 if(gcc_attr_mode ==
"__QI__")
161 else if(gcc_attr_mode ==
"__byte__")
168 else if(gcc_attr_mode ==
"__HI__")
175 else if(gcc_attr_mode ==
"__SI__")
182 else if(gcc_attr_mode ==
"__word__")
189 else if(gcc_attr_mode ==
"__pointer__")
196 else if(gcc_attr_mode ==
"__DI__")
198 if(
config.ansi_c.long_int_width==64)
215 else if(gcc_attr_mode ==
"__TI__")
222 else if(gcc_attr_mode ==
"__V2SI__")
235 else if(gcc_attr_mode ==
"__V4SI__")
265 else if(underlying_type.
id()==ID_floatbv)
269 if(gcc_attr_mode ==
"__SF__")
271 else if(gcc_attr_mode ==
"__DF__")
273 else if(gcc_attr_mode ==
"__TF__")
275 else if(gcc_attr_mode ==
"__V2SF__")
278 else if(gcc_attr_mode ==
"__V2DF__")
281 else if(gcc_attr_mode ==
"__V4SF__")
284 else if(gcc_attr_mode ==
"__V4DF__")
291 type =
result.with_source_location(type);
293 else if(underlying_type.
id()==ID_complex)
298 if(gcc_attr_mode ==
"__SC__")
300 else if(gcc_attr_mode ==
"__DC__")
302 else if(gcc_attr_mode ==
"__TC__")
313 <<
"attribute mode '" << gcc_attr_mode
314 <<
"' applied to inappropriate type '" <<
to_string(type) <<
"'";
320 if(type.
get_bool(ID_C_restricted) &&
321 type.
id()!=ID_pointer &&
325 <<
"only a pointer can be 'restrict'";
333 static_cast<const exprt &
>(type.
find(ID_size));
343 <<
"failed to convert bit vector width to constant";
356 if(type.
id()==ID_custom_unsignedbv)
357 type.
id(ID_unsignedbv);
358 else if(type.
id()==ID_custom_signedbv)
359 type.
id(ID_signedbv);
360 else if(type.
id()==ID_custom_fixedbv)
365 static_cast<const exprt &
>(type.
find(ID_f));
378 <<
"failed to convert number of fraction bits to constant";
381 if(f_int<0 || f_int>size_int)
384 <<
"fixedbv fraction width invalid";
390 else if(type.
id()==ID_custom_floatbv)
395 static_cast<const exprt &
>(type.
find(ID_f));
408 <<
"failed to convert number of fraction bits to constant";
411 if(f_int<1 || f_int+1>=size_int)
414 <<
"floatbv fraction width invalid";
428 exprt width_expr =
static_cast<const exprt &
>(type.
find(ID_width));
438 <<
"failed to convert _BitInt width to constant";
449 <<
"unsigned _BitInt must have at least one bit";
457 <<
"signed _BitInt must have at least two bits";
464 auto bytes = (width_int % 8) == 0 ? width_int / 8 : width_int / 8 + 1;
469 auto width = 8 * bytes_padded;
472 type.
set(ID_C_c_type, type.
id());
489 if(parameters.empty())
496 if(type.
parameters().back().id()==ID_ellipsis)
507 if(param.id()==ID_declaration)
517 std::list<codet> tmp_clean_code;
527 if(identifier.
empty())
542 param.
swap(parameter);
548 if(parameters.size() == 1 && parameters[0].type().id() == ID_empty)
563 if(decl_return_type.
id() == ID_array)
566 <<
"function must not return array";
569 if(decl_return_type.
id() == ID_code)
572 <<
"function must not return function type";
596 <<
"array has incomplete element type";
604 <<
"array of function element type";
631 <<
"failed to convert constant: " << tmp_size.
pretty();
637 <<
"array size must not be negative, "
644 else if(tmp_size.
id()==ID_infinity)
648 else if(tmp_size.
id()==ID_symbol &&
669 <<
"' is not constant";
676 size_source_location,
679 new_symbol.
type.
set(ID_C_constant,
true);
689 assignment.
lhs()=symbol_expr;
690 assignment.
rhs() = new_symbol.
value;
719 if(subtype.
id()!=ID_signedbv &&
720 subtype.
id()!=ID_unsignedbv &&
721 subtype.
id()!=ID_floatbv &&
722 subtype.
id()!=ID_fixedbv)
725 <<
"cannot make a vector of subtype " <<
to_string(subtype);
734 <<
"failed to convert constant: " << size.
pretty();
740 <<
"vector size must be positive, "
748 if(!sub_size_expr_opt.has_value())
751 <<
"failed to determine size of vector base type '" <<
to_string(subtype)
755 simplify(sub_size_expr_opt.value(), *
this);
759 if(!sub_size.has_value())
762 <<
"failed to determine size of vector base type '" <<
to_string(subtype)
769 <<
"type had size 0: '" <<
to_string(subtype) <<
"'";
773 if(s % *sub_size != 0)
776 <<
"vector size (" << s <<
") expected to be multiple of base type size ("
804 remove_qualifiers.
write(type);
806 bool is_packed = type.
get_bool(ID_C_packed);
820 std::string typestr =
type2name(compound_symbol.type, *
this);
821 compound_symbol.base_name =
"#anon#" + typestr;
822 compound_symbol.name=
"tag-#anon#"+typestr;
823 identifier=compound_symbol.name;
836 identifier=type.
find(ID_tag).
get(ID_identifier);
839 symbol_table_baset::symbolst::const_iterator s_it =
847 type.
set(ID_tag, base_name);
854 typet new_type=compound_symbol.type;
873 s_it->second.type.id() == type.
id() &&
881 type.
set(ID_tag, base_name);
884 symbol_table.get_writeable_ref(s_it->first).type.swap(type);
887 else if(s_it->second.type.id() != type.
id())
890 <<
"redefinition of '" << s_it->second.pretty_name <<
"'"
891 <<
" as different kind of tag";
896 <<
"redefinition of body of '" << s_it->second.pretty_name <<
"'";
903 if(type.
id() == ID_union)
905 else if(type.
id() == ID_struct)
913 original_qualifiers.
write(type);
916 type.
set(ID_C_packed,
true);
927 old_components.swap(components);
930 for(
auto &decl : old_components)
941 new_component.
id(ID_static_assert);
945 components.push_back(new_component);
953 for(
const auto &declarator : declaration.
declarators())
956 declarator.get_base_name(), declaration.
full_type(declarator));
962 : declarator.source_location();
973 new_component.
type().
id() != ID_c_bit_field)
980 new_component.
type().
id() != ID_struct_tag &&
981 new_component.
type().
id() != ID_union_tag)
984 <<
"no members defined";
996 new_component.
type().
id() == ID_struct_tag &&
1004 new_component.
type().
id() == ID_union_tag &&
1019 (new_component.
type().
id()!=ID_array ||
1023 <<
"incomplete type not permitted here";
1026 if(new_component.
type().
id() == ID_empty)
1029 <<
"void-typed member not permitted";
1033 new_component.
type().
id() == ID_c_bit_field &&
1038 <<
"zero-width bit-field with declarator not permitted";
1041 components.push_back(new_component);
1046 unsigned anon_member_counter=0;
1049 for(
auto &member : components)
1051 if(!member.get_name().empty())
1054 member.set_name(
"$anon"+std::to_string(anon_member_counter++));
1055 member.set_anonymous(
true);
1061 std::unordered_set<irep_idt> members;
1063 for(
const auto &c : components)
1065 if(!members.insert(c.get_name()).second)
1068 <<
"duplicate member '" << c.get_name() <<
'\'';
1076 if(type.
id()==ID_struct ||
1077 type.
id()==ID_union)
1079 for(struct_union_typet::componentst::iterator
1080 it=components.begin();
1081 it!=components.end();
1084 typet &c_type=it->type();
1086 if(c_type.
id()==ID_array &&
1090 if(type.
id()==ID_struct && it!=--components.end())
1093 <<
"flexible struct member must be last member";
1098 c_type.
set(ID_C_flexible_array_member,
true);
1107 if(type.
id()==ID_struct)
1109 else if(type.
id()==ID_union)
1113 for(struct_union_typet::componentst::iterator
1114 it=components.begin();
1115 it!=components.end();
1118 if(it->id()==ID_static_assert)
1123 <<
"static_assert not supported in compound body";
1135 <<
"failed _Static_assert";
1142 it=components.erase(it);
1151 components.empty() &&
1155 <<
"C requires that a struct or union has at least one member";
1194 bool is_packed)
const
1264 const bool have_underlying_type =
1267 if(have_underlying_type)
1271 const typet &underlying_type =
1272 static_cast<const typet &
>(type.
find(ID_enum_underlying_type));
1277 <<
"non-integral type '" << underlying_type.
get(ID_C_c_type)
1278 <<
"' is an invalid underlying type";
1284 mp_integer value=0, min_value=0, max_value=0;
1286 std::vector<c_enum_typet::c_enum_membert> enum_members;
1287 enum_members.reserve(as_expr.
operands().size());
1317 <<
"enum is not a constant";
1326 typet constant_type;
1328 if(have_underlying_type)
1330 constant_type = type.
find_type(ID_enum_underlying_type);
1333 if(value < tmp.smallest() || value > tmp.largest())
1336 <<
"enumerator value is not representable in the underlying type '"
1337 << constant_type.
get(ID_C_c_type) <<
"'";
1347 declaration.
type()=constant_type;
1363 enum_members.push_back(member);
1373 bool is_packed=type.
get_bool(ID_C_packed);
1378 if(have_underlying_type)
1389 std::size_t width = underlying_type.
get_width();
1390 for(
auto &member : enum_members)
1402 std::string anon_identifier=
"#anon_enum";
1404 for(
const auto &member : enum_members)
1406 anon_identifier+=
'$';
1407 anon_identifier+=
id2string(member.get_base_name());
1408 anon_identifier+=
'=';
1409 anon_identifier+=
id2string(member.get_value());
1413 anon_identifier+=
"#packed";
1415 type.
add(ID_tag).
set(ID_identifier, anon_identifier);
1424 enum_tag_symbol.
location=source_location;
1425 enum_tag_symbol.is_file_local=
true;
1426 enum_tag_symbol.base_name=base_name;
1428 enum_tag_symbol.type.add_subtype() = underlying_type;
1439 const symbolt &symbol = *existing_symbol;
1441 if(symbol.
type.
id() != ID_c_enum)
1444 <<
"use of tag that does not match previous declaration";
1451 existing_symbol->
type = enum_tag_symbol.type;
1458 if(!base_name.
empty())
1461 <<
"redeclaration of enum tag";
1472 type.
id(ID_c_enum_tag);
1474 type.
set(ID_identifier, identifier);
1484 <<
"anonymous enum tag without members";
1490 warning() <<
"ignoring specification of underlying type for enum" <<
eom;
1500 symbol_table_baset::symbolst::const_iterator s_it =
1506 const symbolt &symbol=s_it->second;
1508 if(symbol.
type.
id() != ID_c_enum)
1511 <<
"use of tag that does not match previous declaration";
1518 new_type.
add(ID_tag)=tag;
1522 enum_tag_symbol.
location=source_location;
1523 enum_tag_symbol.is_file_local=
true;
1524 enum_tag_symbol.base_name=base_name;
1550 <<
"failed to convert bit field width";
1556 <<
"bit field width is negative";
1565 std::size_t sub_width=0;
1567 if(underlying_type.
id() == ID_bool)
1573 underlying_type.
id() == ID_signedbv ||
1574 underlying_type.
id() == ID_unsignedbv || underlying_type.
id() == ID_c_bool)
1578 else if(underlying_type.
id() == ID_c_enum_tag)
1583 const auto &c_enum_type =
1586 if(c_enum_type.is_incomplete())
1589 <<
"bit field has incomplete enum type";
1597 <<
"bit field with non-integer type: " <<
to_string(underlying_type);
1603 <<
"bit field (" << i <<
" bits) larger than type (" << sub_width
1615 c_qualifiers.
read(type);
1617 const auto &as_expr = (
const exprt &)type;
1619 if(!as_expr.has_operands())
1631 if(expr.
id()==ID_address_of &&
1641 c_qualifiers.
write(type);
1648 symbol_table_baset::symbolst::const_iterator s_it =
1654 <<
"typedef symbol '" << identifier <<
"' not found";
1657 const symbolt &symbol = s_it->second;
1662 <<
"expected type symbol for typedef";
1668 bool is_packed = type.
get_bool(ID_C_packed);
1673 c_qualifiers.
write(type);
1676 type.
set(ID_C_packed,
true);
1693 if(type.
id()==ID_array)
1699 else if(type.
id()==ID_code)
1707 else if(type.
id()==ID_KnR)
ANSI-C Language Conversion.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
ANSI-C Language Type Checking.
already_typechecked_typet & to_already_typechecked_type(typet &type)
floatbv_typet float_type()
signedbv_typet signed_long_int_type()
signedbv_typet signed_char_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_char_type()
signedbv_typet signed_size_type()
signedbv_typet signed_long_long_int_type()
bitvector_typet c_index_type()
floatbv_typet double_type()
signedbv_typet signed_short_int_type()
unsignedbv_typet unsigned_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.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
static void make_already_typechecked(typet &type)
virtual void write(typet &type)
const ansi_c_declaratort & declarator() const
const declaratorst & declarators() const
typet full_type(const ansi_c_declaratort &) const
bool get_is_static_assert() const
irep_idt get_base_name() const
irep_idt get_name() const
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
typet & index_type_nonconst()
The type of the index expressions into any instance of this type.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
std::size_t width() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
const typet & underlying_type() const
C enum tag type, i.e., c_enum_typet with an identifier.
void set_identifier(const irep_idt &identifier)
void set_value(const irep_idt &value)
void set_base_name(const irep_idt &base_name)
void make_incomplete()
enum types may be incomplete
bool is_incomplete() const
enum types may be incomplete
virtual void write(typet &src) const
virtual void read(const typet &src)
bool is_transparent_union
symbol_table_baset & symbol_table
virtual void typecheck_compound_body(struct_union_typet &type)
virtual void make_index_type(exprt &expr)
virtual void typecheck_code_type(code_typet &type)
virtual void typecheck_expr(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_vector_type(typet &type)
virtual void typecheck_c_enum_type(typet &type)
virtual void make_constant(exprt &expr)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
virtual void adjust_function_parameter(typet &type) const
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
virtual void typecheck_custom_type(typet &type)
virtual void make_constant_index(exprt &expr)
bitvector_typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual void typecheck_compound_type(struct_union_typet &type)
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_typedef_type(typet &type)
virtual void typecheck_bitint_type(typet &)
virtual void typecheck_array_type(array_typet &type)
virtual void typecheck_typeof_type(typet &type)
virtual void typecheck_type(typet &type)
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
void set_base_name(const irep_idt &name)
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
Complex numbers made of pair of given subtype.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
Unbounded, signed integers (mathematical integers, not bitvectors)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & warning() const
mstreamt & result() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Unbounded, signed rational numbers.
A struct tag type, i.e., struct_typet with an identifier.
void set_pretty_name(const irep_idt &name)
const irep_idt & get_name() const
Base type for structs and unions.
const componentst & components() const
void make_incomplete()
A struct/union may be incomplete.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
const irep_idt & get_identifier() const
void set_identifier(const irep_idt &identifier)
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
errort with_location(source_locationt _location) &&
const irep_idt & get_identifier() const
The type of an expression, extends irept.
typet & add_type(const irep_idt &name)
const typet & find_type(const irep_idt &name) const
source_locationt & add_source_location()
const source_locationt & source_location() const
typet && with_source_location(source_locationt location) &&
This is a 'fluent style' method for creating a new type with an added-on source location.
A union tag type, i.e., union_typet with an identifier.
const constant_exprt & size() const
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 ...
Fresh auxiliary symbol creation.
signedbv_typet gcc_signed_int128_type()
unsignedbv_typet gcc_unsigned_int128_type()
floatbv_typet gcc_float128_type()
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
mp_integer alignment(const typet &type, const namespacet &ns)
void add_padding(struct_typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
const type_with_subtypet & to_type_with_subtype(const typet &type)
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
bool is_signed(const typet &t)
Convenience function – is the type signed?