Go to the documentation of this file.
13 #ifndef CPROVER_UTIL_STD_TYPES_H
14 #define CPROVER_UTIL_STD_TYPES_H
23 #include <unordered_map>
81 return set(ID_name, name);
86 return get(ID_base_name);
91 return set(ID_base_name, base_name);
96 return get(ID_access);
101 return set(ID_access, access);
106 return get(ID_pretty_name);
111 return set(ID_pretty_name, name);
121 return set(ID_anonymous, anonymous);
131 return set(ID_C_is_padding, is_padding);
158 const irep_idt &component_name)
const;
169 return id() == ID_struct &&
get_bool(ID_C_class);
176 return is_class() ? ID_private : ID_public;
188 set(ID_incomplete,
true);
198 return type.
id() == ID_struct || type.
id() == ID_union;
292 return type.
id() == ID_struct;
324 set(ID_C_class,
true);
411 return type.
id() == ID_union;
448 set(ID_identifier, identifier);
453 return get(ID_identifier);
463 return type.
id() == ID_c_enum_tag || type.
id() == ID_struct_tag ||
464 type.
id() == ID_union_tag;
478 return static_cast<const tag_typet &
>(type);
504 return type.
id() == ID_struct_tag;
544 return type.
id() == ID_union_tag;
594 return type.
id() == ID_enumeration;
635 set(ID_identifier, identifier);
640 set(ID_base_name, base_name);
660 set(ID_incomplete,
true);
670 return type.
id() == ID_c_enum;
710 return type.
id() == ID_c_enum_tag;
776 return add_expr(ID_C_default_value);
784 set(ID_C_identifier, identifier);
789 set(ID_C_base_name, name);
794 return get(ID_C_identifier);
799 return get(ID_C_base_name);
809 set(ID_C_this,
true);
826 if(!p.empty() && p.front().get_this())
839 add(ID_parameters).
set(ID_ellipsis,
true);
874 set(ID_C_inlined, value);
879 return get(ID_access);
884 return set(ID_access, access);
894 set(ID_constructor,
true);
900 std::vector<irep_idt> result;
902 result.reserve(p.size());
903 for(parameterst::const_iterator it=p.begin();
905 result.push_back(it->get_identifier());
917 std::size_t index = 0;
918 for(
const auto &p : params)
920 const irep_idt &
id = p.get_identifier();
935 return type.
id() == ID_code;
970 add(ID_size, std::move(_size));
975 return static_cast<const exprt &
>(
find(ID_size));
980 return static_cast<exprt &
>(
add(ID_size));
1000 return type.
id() == ID_array;
1048 set(ID_width, narrow_cast<long long>(width));
1056 vm, !type.
get(ID_width).
empty(),
"bitvector type must have width");
1066 return type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
1067 type.
id() == ID_fixedbv || type.
id() == ID_floatbv ||
1068 type.
id() == ID_verilog_signedbv ||
1069 type.
id() == ID_verilog_unsignedbv || type.
id() == ID_bv ||
1070 type.
id() == ID_pointer || type.
id() == ID_c_bit_field ||
1071 type.
id() == ID_c_bool;
1078 return type.
id() == ID_signedbv || type.
id() == ID_unsignedbv;
1118 vm, !type.
get(ID_width).
empty(),
"bitvector type must have width");
1128 return type.
id() == ID_bv;
1143 return static_cast<const bv_typet &
>(type);
1151 return static_cast<bv_typet &
>(type);
1187 return type.
id() == ID_signedbv || type.
id() == ID_unsignedbv;
1237 return type.
id() == ID_unsignedbv;
1277 vm, !type.
get(ID_width).
empty(),
"signed bitvector type must have width");
1287 return type.
id() == ID_signedbv;
1333 set(ID_integer_bits, narrow_cast<long long>(b));
1341 vm, !type.
get(ID_width).
empty(),
"fixed bitvector type must have width");
1351 return type.
id() == ID_fixedbv;
1391 std::size_t
get_f()
const;
1395 set(ID_f, narrow_cast<long long>(b));
1403 vm, !type.
get(ID_width).
empty(),
"float bitvector type must have width");
1413 return type.
id() == ID_floatbv;
1460 return type.
id() == ID_c_bit_field;
1515 return type.
id() == ID_pointer;
1545 return type.
id() == ID_pointer && type.
subtype().
id() == ID_empty;
1558 set(ID_C_reference,
true);
1625 return type.
id() == ID_c_bool;
1668 return type.
id() == ID_string;
1715 return type.
id() == ID_range;
1764 return type.
id() == ID_vector;
1804 return type.
id() == ID_complex;
1832 #endif // CPROVER_UTIL_STD_TYPES_H
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const irep_idt & get_identifier() const
void set_f(std::size_t b)
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
bool has_ellipsis() const
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
struct_tag_typet(const irep_idt &identifier)
void set_identifier(const irep_idt &identifier)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
const typet & subtype() const
bool is_incomplete() const
const exprt & find_expr(const irep_idt &name) const
c_enum_typet(typet _subtype)
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
void set_value(const irep_idt &value)
bool get_anonymous() const
componentt(const irep_idt &_name, typet _type)
bool is_incomplete() const
enum types may be incomplete
void set_integer_bits(std::size_t b)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
void set_access(const irep_idt &access)
An enumeration type, i.e., a type with elements (not to be confused with C enums)
void set_anonymous(bool anonymous)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
The type of an expression, extends irept.
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
std::vector< parametert > parameterst
c_bit_field_typet(typet _subtype, std::size_t width)
tag_typet(const irep_idt &_id, const irep_idt &identifier)
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Base type for structs and unions.
std::size_t get_f() const
void set_identifier(const irep_idt &identifier)
bool can_cast_type< bv_typet >(const typet &type)
Check whether a reference to a typet is a bv_typet.
std::vector< c_enum_membert > memberst
irept & add(const irep_namet &name)
static_memberst & static_members()
Fixed-width bit-vector with IEEE floating-point interpretation.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
const irept & find(const irep_namet &name) const
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
unsignedbv_typet(std::size_t width)
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
const typet & component_type(const irep_idt &component_name) const
Base class for all expressions.
std::vector< componentt > componentst
const irep_idt & get_access() const
A struct tag type, i.e., struct_typet with an identifier.
Complex numbers made of pair of given subtype.
void make_incomplete()
enum types may be incomplete
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const irep_idt & get_pretty_name() const
void make_incomplete()
A struct/union may be incomplete.
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Type with a single subtype.
std::unordered_map< irep_idt, std::size_t > parameter_indicest
irep_idt get_base_name() const
bool is_reference(const typet &type)
Returns true if the type is a reference.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
bool can_cast_type< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
void set_name(const irep_idt &name)
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
bool get_is_constructor() const
A union tag type, i.e., union_typet with an identifier.
const parametert * get_this() const
Fixed-width bit-vector with unsigned binary interpretation.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
componentst & components()
union_typet(componentst _components)
const exprt & size() const
struct_union_typet(const irep_idt &_id)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
bool is_class() const
A struct may be a class, where members may have access restrictions.
bool can_cast_type< struct_typet >(const typet &type)
Check whether a reference to a typet is a struct_typet.
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
struct_union_typet(const irep_idt &_id, componentst _components)
componentst static_memberst
const irep_idt & get_base_name() const
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const irep_idt & get_access() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
bitvector_typet(const irep_idt &_id, std::size_t width)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
bool can_cast_type< fixedbv_typet >(const typet &type)
Check whether a reference to a typet is a fixedbv_typet.
const irep_idt & get_name() const
void set_tag(const irep_idt &tag)
bool can_cast_type< c_bit_field_typet >(const typet &type)
Check whether a reference to a typet is a c_bit_field_typet.
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
signedbv_typet(std::size_t width)
void set_is_constructor()
const exprt & default_value() const
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
mp_integer get_from() const
struct_typet(componentst _components)
complex_typet(typet _subtype)
#define PRECONDITION(CONDITION)
pointer_typet(typet _subtype, std::size_t width)
bool get_is_padding() const
void set_pretty_name(const irep_idt &name)
Fixed-width bit-vector with two's complement interpretation.
integer_bitvector_typet(const irep_idt &id, std::size_t width)
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
code_typet(parameterst _parameters, typet _return_type)
Constructs a new code type, i.e., function type.
void set_base_name(const irep_idt &base_name)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
A type for subranges of integers.
void set_inlined(bool value)
const static_memberst & static_members() const
bool is_class() const
A struct may be a class, where members may have access restrictions.
Fixed-width bit-vector representing a signed or unsigned integer.
c_bool_typet(std::size_t width)
std::size_t get_e() const
const basest & bases() const
Get the collection of base classes/structs.
void set_identifier(const irep_idt &identifier)
void validate_type(const reference_typet &type)
bitvector_typet(const irep_idt &_id)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
bool has_component(const irep_idt &component_name) const
mp_integer get_to() const
const irep_idt & id() const
std::vector< baset > basest
bool can_cast_type< union_tag_typet >(const typet &type)
Check whether a reference to a typet is a union_tag_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void remove(const irep_namet &name)
A tag-based type, i.e., typet with an identifier.
tree_implementationt baset
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
reference_typet(typet _subtype, std::size_t _width)
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
#define SINCE(year, month, day, msg)
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
nonstd::optional< T > optionalt
const constant_exprt & size() const
struct_tag_typet & type()
void set_width(std::size_t width)
void set_is_padding(bool is_padding)
irep_idt get_value() const
basest & bases()
Get the collection of base classes/structs.
range_typet(const mp_integer &_from, const mp_integer &_to)
void set_base_name(const irep_idt &name)
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Fixed-width bit-vector with signed fixed-point interpretation.
std::size_t get_width() const
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
c_enum_tag_typet(const irep_idt &identifier)
const irept::subt & elements() const
vector_typet(const typet &_subtype, const constant_exprt &_size)
void set_to(const mp_integer &to)
Structure type, corresponds to C style structs.
const methodst & methods() const
C enum tag type, i.e., c_enum_typet with an identifier.
std::size_t get_size_t(const irep_namet &name) const
std::size_t get_fraction_bits() const
exprt & add_expr(const irep_idt &name)
void set_base_name(const irep_idt &base_name)
Base class of fixed-width bit-vector types.
const irep_idt & get(const irep_namet &name) const
parametert(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
std::size_t get_integer_bits() const
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Templated functions to cast to specific exprt-derived classes.
const irep_idt & get_identifier() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool can_cast_type< c_enum_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
union_tag_typet(const irep_idt &identifier)
mp_integer largest() const
Return the largest value that can be represented using this type.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const typet & return_type() const
array_typet(typet _subtype, exprt _size)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
typet & add_type(const irep_namet &name)
irep_idt get_identifier() const
bv_typet(std::size_t width)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
const irep_idt & get_base_name() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
const typet & find_type(const irep_namet &name) const
A constant literal expression.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
bool is_incomplete() const
A struct/union may be incomplete.
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_typet.
bool can_cast_type< struct_union_typet >(const typet &type)
Check whether a reference to a typet is a struct_union_typet.
void set_access(const irep_idt &access)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
signedbv_typet difference_type() const
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Fixed-width bit-vector without numerical interpretation.
parameterst & parameters()
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
void set_from(const mp_integer &_from)
const memberst & members() const
bool has_default_value() const
Base class for tree-like data structures with sharing.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)