Go to the documentation of this file.
13 #ifndef CPROVER_UTIL_STD_TYPES_H
14 #define CPROVER_UTIL_STD_TYPES_H
22 #include <unordered_map>
72 set(ID_identifier, identifier);
77 return get(ID_identifier);
87 return type.
id() == ID_symbol_type;
139 return set(ID_name, name);
144 return get(ID_base_name);
149 return set(ID_base_name, base_name);
154 return get(ID_access);
159 return set(ID_access, access);
164 return get(ID_pretty_name);
169 return set(ID_pretty_name, name);
179 return set(ID_anonymous, anonymous);
189 return set(ID_C_is_padding, is_padding);
199 set(ID_final, is_final);
221 const irep_idt &component_name)
const;
232 return id() == ID_struct &&
get_bool(ID_C_class);
239 return is_class() ? ID_private : ID_public;
249 return type.
id() == ID_struct || type.
id() == ID_union;
338 return type.
id() == ID_struct;
370 set(ID_C_class,
true);
439 return type.
id() == ID_union;
476 set(ID_identifier, identifier);
481 return get(ID_identifier);
491 return type.
id() == ID_c_enum_tag || type.
id() == ID_struct_tag ||
492 type.
id() == ID_union_tag;
506 return static_cast<const tag_typet &
>(type);
532 return type.
id() == ID_struct_tag;
572 return type.
id() == ID_union_tag;
622 return type.
id() == ID_enumeration;
663 set(ID_identifier, identifier);
668 set(ID_base_name, base_name);
686 return type.
id() == ID_c_enum;
726 return type.
id() == ID_c_enum_tag;
777 DEPRECATED(
"Use the two argument constructor instead")
812 return add_expr(ID_C_default_value);
820 set(ID_C_identifier, identifier);
825 set(ID_C_base_name, name);
830 return get(ID_C_identifier);
835 return get(ID_C_base_name);
845 set(ID_C_this,
true);
862 if(!p.empty() && p.front().get_this())
875 add(ID_parameters).
set(ID_ellipsis,
true);
910 set(ID_C_inlined, value);
915 return get(ID_access);
920 return set(ID_access, access);
930 set(ID_constructor,
true);
936 std::vector<irep_idt> result;
938 result.reserve(p.size());
939 for(parameterst::const_iterator it=p.begin();
941 result.push_back(it->get_identifier());
953 std::size_t index = 0;
956 const irep_idt &
id = p.get_identifier();
971 return type.
id() == ID_code;
1004 const typet &_subtype,
1012 return static_cast<const exprt &
>(
find(ID_size));
1017 return static_cast<exprt &
>(
add(ID_size));
1037 return type.
id() == ID_array;
1076 return type.
id() == ID_incomplete_array;
1124 set(ID_width, width);
1132 vm, !type.
get(ID_width).
empty(),
"bitvector type must have width");
1142 return type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
1143 type.
id() == ID_fixedbv || type.
id() == ID_floatbv ||
1144 type.
id() == ID_verilog_signedbv ||
1145 type.
id() == ID_verilog_unsignedbv || type.
id() == ID_bv ||
1146 type.
id() == ID_pointer || type.
id() == ID_c_bit_field ||
1147 type.
id() == ID_c_bool;
1189 return type.
id() == ID_bv;
1251 return type.
id() == ID_unsignedbv;
1299 return type.
id() == ID_signedbv;
1305 !type.
get(ID_width).
empty(),
"signed bitvector type must have width");
1353 set(ID_integer_bits, b);
1363 return type.
id() == ID_fixedbv;
1369 !type.
get(ID_width).
empty(),
"fixed bitvector type must have width");
1411 std::size_t
get_f()
const;
1425 return type.
id() == ID_floatbv;
1431 !type.
get(ID_width).
empty(),
"float bitvector type must have width");
1480 return type.
id() == ID_c_bit_field;
1528 return type.
id() == ID_pointer;
1571 set(ID_C_reference,
true);
1626 return type.
id() == ID_c_bool;
1676 return type.
id() == ID_string;
1723 return type.
id() == ID_range;
1759 const typet &_subtype,
1767 return static_cast<const exprt &
>(
find(ID_size));
1772 return static_cast<exprt &
>(
add(ID_size));
1782 return type.
id() == ID_vector;
1810 DEPRECATED(
"use complex_typet(type) instead")
1827 return type.
id() == ID_complex;
1855 #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
#define PRECONDITION(CONDITION)
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
constant_exprt largest_expr() const
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
code_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e., function type.
mp_integer smallest() const
void set_integer_bits(std::size_t b)
constant_exprt zero_expr() const
const exprt & size() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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.
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
void set_is_final(const bool is_final)
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.
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.
void set_identifier(const irep_idt &identifier)
std::vector< c_enum_membert > memberst
irept & add(const irep_namet &name)
bool get_is_final() const
Fixed-width bit-vector with IEEE floating-point interpretation.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
bool can_cast_type< incomplete_array_typet >(const typet &type)
Check whether a reference to a typet is a incomplete_array_typet.
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
The NIL type, i.e., an invalid type, no value.
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
c_bit_field_typet(const typet &_subtype, std::size_t width)
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)
constant_exprt largest_expr() const
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
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a typet to an incomplete_array_typet.
A struct tag type, i.e., struct_typet with an identifier.
Complex numbers made of pair of given subtype.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const irep_idt & get_pretty_name() const
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
constant_exprt smallest_expr() const
irep_idt get_base_name() const
bool is_reference(const typet &type)
Returns true if the type is a reference.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const irep_idt & get_identifier() const
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)
bool get_is_constructor() const
A union tag type, i.e., union_typet with an identifier.
const parametert * get_this() const
c_enum_typet(const typet &_subtype)
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()
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 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.
pointer_typet(const typet &_subtype, std::size_t width)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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.
The void type, the same as empty_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)
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()
mp_integer smallest() const
const exprt & default_value() const
baset(const struct_tag_typet &base)
mp_integer get_from() const
bool can_cast_type< symbol_typet >(const typet &type)
Check whether a reference to a typet is a symbol_typet.
bool get_is_padding() const
void set_pretty_name(const irep_idt &name)
Fixed-width bit-vector with two's complement interpretation.
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
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)
bool is_class() const
A struct may be a class, where members may have access restrictions.
c_bool_typet(std::size_t width)
vector_typet(const typet &_subtype, const exprt &_size)
std::size_t get_e() const
const basest & bases() const
Get the collection of base classes/structs.
void set_identifier(const irep_idt &identifier)
bitvector_typet(const irep_idt &_id)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
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.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
mp_integer largest() const
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
nonstd::optional< T > optionalt
void set_width(std::size_t width)
void set_is_padding(bool is_padding)
constant_exprt smallest_expr() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
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)
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
c_enum_tag_typet(const irep_idt &identifier)
reference_typet(const typet &_subtype, std::size_t _width)
const irept::subt & elements() const
componentt(const irep_idt &_name, const typet &_type)
void set_to(const mp_integer &to)
Structure type, corresponds to C style structs.
void validate_type(const bv_typet &type)
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.
constant_exprt zero_expr() const
const irep_idt & get(const irep_namet &name) const
parametert(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
struct_tag_typet & type()
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.
complex_typet(const typet &_subtype)
Templated functions to cast to specific exprt-derived classes.
const irep_idt & get_identifier() const
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.
mp_integer largest() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
array_typet(const typet &_subtype, const exprt &_size)
union_tag_typet(const irep_idt &identifier)
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const typet & return_type() const
Base class for tree-like data structures with sharing.
const irept & get_nil_irep()
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
A reference into the symbol table.
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.
symbol_typet(const irep_idt &identifier)
std::vector< irept > subt
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)
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()
Base class or struct that a class or struct inherits from.
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
code_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e., function type.
bool has_default_value() const