14#include <unordered_set>
57 type = already_typechecked.
get_type();
59 c_qualifiers.
write(type);
305 <<
"' applied to inappropriate type '" <<
to_string(type) <<
"'"
318 error() <<
"only a pointer can be 'restrict'" <<
eom;
337 error() <<
"failed to convert bit vector width to constant" <<
eom;
344 error() <<
"bit vector width invalid" <<
eom;
365 f_expr.find_source_location();
375 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
382 error() <<
"fixedbv fraction width invalid" <<
eom;
397 f_expr.find_source_location();
407 error() <<
"failed to convert number of fraction bits to constant" <<
eom;
414 error() <<
"floatbv fraction width invalid" <<
eom;
434 if(parameters.empty())
472 if(identifier.
empty())
493 if(parameters.size() == 1 && parameters[0].type().id() ==
ID_empty)
511 error() <<
"function must not return array" <<
eom;
518 error() <<
"function must not return function type" <<
eom;
548 error() <<
"array has incomplete element type" <<
eom;
557 error() <<
"array of function element type" <<
eom;
581 error() <<
"failed to convert constant: "
589 error() <<
"array size must not be negative, "
590 "but got " << s <<
eom;
621 <<
"' is not constant" <<
eom;
642 assignment.
lhs()=symbol_expr;
643 assignment.
rhs() = new_symbol.
value;
678 error() <<
"cannot make a vector of subtype "
689 error() <<
"failed to convert constant: "
697 error() <<
"vector size must be positive, "
698 "but got " << s <<
eom;
708 error() <<
"failed to determine size of vector base type '"
720 error() <<
"failed to determine size of vector base type '"
736 error() <<
"vector size (" << s
737 <<
") expected to be multiple of base type size (" << *
sub_size
746 new_type.add_source_location() = source_location;
747 new_type.size().add_source_location() = source_location;
803 symbol_tablet::symbolst::const_iterator
s_it=
840 s_it->second.type.id() == type.
id() &&
854 else if(
s_it->second.type.id() != type.
id())
857 error() <<
"redefinition of '" <<
s_it->second.pretty_name <<
"'"
858 <<
" as different kind of tag" <<
eom;
864 error() <<
"redefinition of body of '" <<
s_it->second.pretty_name
923 for(
const auto &declarator :
declaration.declarators())
926 declarator.get_base_name(),
declaration.full_type(declarator));
931 declarator.get_name().empty() ?
declaration.source_location()
932 : declarator.source_location();
944 error() <<
"incomplete type not permitted here" <<
eom;
951 error() <<
"void-typed member not permitted" <<
eom;
963 for(
auto &member : components)
965 if(!member.get_name().empty())
969 member.set_anonymous(
true);
975 std::unordered_set<irep_idt> members;
977 for(
const auto &
c : components)
979 if(!members.insert(
c.get_name()).second)
982 error() <<
"duplicate member '" <<
c.get_name() <<
'\'' <<
eom;
994 for(struct_union_typet::componentst::iterator
995 it=components.begin();
996 it!=components.end();
1005 if(type.
id()==
ID_struct && it!=--components.end())
1008 error() <<
"flexible struct member must be last member" <<
eom;
1030 for(struct_typet::componentst::iterator
1031 it=components.begin();
1032 it!=components.end();
1037 it=components.erase(it);
1043 for(struct_union_typet::componentst::iterator
1044 it=components.begin();
1045 it!=components.end();
1053 error() <<
"static_assert not supported in compound body" <<
eom;
1066 error() <<
"failed _Static_assert" <<
eom;
1074 it=components.erase(it);
1195 const typet &underlying_type =
1200 std::ostringstream msg;
1201 msg << source_location <<
": non-integral type '"
1203 <<
"' is an invalid underlying type";
1210 mp_integer value=0, min_value=0, max_value=0;
1233 else if(
tmp_v.is_false())
1243 error() <<
"enum is not a constant" <<
eom;
1260 if(value <
tmp.smallest() || value >
tmp.largest())
1262 std::ostringstream msg;
1265 <<
": enumerator value is not representable in the underlying type '"
1319 std::size_t width = underlying_type.
get_width();
1366 body.push_back(member);
1371 symbol_tablet::symbolst::const_iterator
s_it=
1382 error() <<
"use of tag that does not match previous declaration" <<
eom;
1397 if(!base_name.
empty())
1400 error() <<
"redeclaration of enum tag" <<
eom;
1424 error() <<
"anonymous enum tag without members" <<
eom;
1431 warning() <<
"ignoring specification of underlying type for enum" <<
eom;
1441 symbol_tablet::symbolst::const_iterator
s_it=
1452 error() <<
"use of tag that does not match previous declaration" <<
eom;
1496 error() <<
"failed to convert bit field width" <<
eom;
1503 error() <<
"bit field width is negative" <<
eom;
1537 error() <<
"bit field has incomplete enum type" <<
eom;
1546 error() <<
"bit field with non-integer type: " <<
to_string(underlying_type)
1554 error() <<
"bit field (" <<
i
1555 <<
" bits) larger than type (" <<
sub_width <<
" bits)"
1568 c_qualifiers.
read(type);
1570 const auto &as_expr = (
const exprt &)type;
1572 if(!as_expr.has_operands())
1594 c_qualifiers.
write(type);
1601 symbol_tablet::symbolst::const_iterator
s_it =
1607 error() <<
"typedef symbol '" << identifier <<
"' not found" <<
eom;
1616 error() <<
"expected type symbol for typedef" <<
eom;
1628 c_qualifiers.
write(type);
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 enum_constant_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.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static void make_already_typechecked(typet &type)
bool is_incomplete() const
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
Base class of fixed-width bit-vector types.
void set_width(std::size_t width)
std::size_t get_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)
bool is_incomplete() const
enum types may be incomplete
virtual void write(typet &src) const override
virtual void read(const typet &src) override
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)
symbol_tablet & symbol_table
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)
const irep_idt const irep_idt mode
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_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.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
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)
Thrown when we can't handle something in an input source file.
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 typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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.
Base type for structs and unions.
const componentst & components() const
bool is_incomplete() const
A struct/union may be incomplete.
void make_incomplete()
A struct/union may be incomplete.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
const irep_idt & get_identifier() const
void set_identifier(const irep_idt &identifier)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
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
const typet & subtype() const
source_locationt & add_source_location()
const source_locationt & source_location() const
A union tag type, i.e., union_typet with an identifier.
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.
optionalt< 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 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 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 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?