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>
80 return set(ID_name, name);
85 return get(ID_base_name);
90 return set(ID_base_name, base_name);
95 return get(ID_access);
100 return set(ID_access, access);
105 return get(ID_pretty_name);
110 return set(ID_pretty_name, name);
120 return set(ID_anonymous, anonymous);
130 return set(ID_C_is_padding, is_padding);
157 const irep_idt &component_name)
const;
168 return id() == ID_struct &&
get_bool(ID_C_class);
175 return is_class() ? ID_private : ID_public;
187 set(ID_incomplete,
true);
197 return type.
id() == ID_struct || type.
id() == ID_union;
291 return type.
id() == ID_struct;
323 set(ID_C_class,
true);
401 set(ID_identifier, identifier);
406 return get(ID_identifier);
416 return type.
id() == ID_c_enum_tag || type.
id() == ID_struct_tag ||
417 type.
id() == ID_union_tag;
431 return static_cast<const tag_typet &
>(type);
457 return type.
id() == ID_struct_tag;
507 return type.
id() == ID_enumeration;
568 return add_expr(ID_C_default_value);
576 set(ID_C_identifier, identifier);
581 set(ID_C_base_name, name);
586 return get(ID_C_identifier);
591 return get(ID_C_base_name);
601 set(ID_C_this,
true);
618 if(!p.empty() && p.front().get_this())
631 add(ID_parameters).
set(ID_ellipsis,
true);
666 set(ID_C_inlined, value);
671 return get(ID_access);
676 return set(ID_access, access);
686 set(ID_constructor,
true);
692 std::vector<irep_idt> result;
694 result.reserve(p.size());
695 for(parameterst::const_iterator it=p.begin();
697 result.push_back(it->get_identifier());
709 std::size_t index = 0;
710 for(
const auto &p : params)
712 const irep_idt &
id = p.get_identifier();
727 return type.
id() == ID_code;
762 add(ID_size, std::move(_size));
767 return static_cast<const exprt &
>(
find(ID_size));
772 return static_cast<exprt &
>(
add(ID_size));
796 return type.
id() == ID_array;
852 vm, !type.
get(ID_width).
empty(),
"bitvector type must have width");
862 return type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
863 type.
id() == ID_fixedbv || type.
id() == ID_floatbv ||
864 type.
id() == ID_verilog_signedbv ||
865 type.
id() == ID_verilog_unsignedbv || type.
id() == ID_bv ||
866 type.
id() == ID_pointer || type.
id() == ID_c_bit_field ||
867 type.
id() == ID_c_bool;
887 return type.
id() == ID_string;
934 return type.
id() == ID_range;
983 return type.
id() == ID_vector;
1023 return type.
id() == ID_complex;
1051 #endif // CPROVER_UTIL_STD_TYPES_H
const irep_idt & get_identifier() const
const componentst & components() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
bool is_incomplete() const
const exprt & find_expr(const irep_idt &name) const
bool get_anonymous() const
componentt(const irep_idt &_name, typet _type)
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.
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.
The type of an expression, extends irept.
std::vector< parametert > parameterst
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.
void set_identifier(const irep_idt &identifier)
irept & add(const irep_namet &name)
static_memberst & static_members()
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.
const irept & find(const irep_namet &name) const
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.
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.
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
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)
bool get_is_constructor() const
const parametert * get_this() const
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.
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 irep_idt & get_access() const
bitvector_typet(const irep_idt &_id, std::size_t width)
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
const irep_idt & get_name() const
void set_tag(const irep_idt &tag)
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
void set_is_constructor()
const exprt & default_value() const
mp_integer get_from() const
struct_typet(componentst _components)
complex_typet(typet _subtype)
#define PRECONDITION(CONDITION)
bool get_is_padding() const
void set_pretty_name(const irep_idt &name)
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)
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.
const basest & bases() const
Get the collection of base classes/structs.
bitvector_typet(const irep_idt &_id)
bool has_component(const irep_idt &component_name) const
mp_integer get_to() const
const irep_idt & id() const
std::vector< baset > basest
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)
const parameterst & parameters() const
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)
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)
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.
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.
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
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
std::size_t get_size_t(const irep_namet &name) const
exprt & add_expr(const irep_idt &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)
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
void set_size_t(const irep_namet &name, const std::size_t value)
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.
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)
typet & add_type(const irep_namet &name)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
const irep_idt & get_base_name() const
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)
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
parameterst & parameters()
void set_from(const mp_integer &_from)
bool has_default_value() const
Base class for tree-like data structures with sharing.