10 #ifndef CPROVER_UTIL_STD_TYPES_H 11 #define CPROVER_UTIL_STD_TYPES_H 123 set(ID_identifier, identifier);
128 return get(ID_identifier);
144 assert(type.
id()==ID_symbol);
153 assert(type.
id()==ID_symbol);
186 return set(ID_name, name);
191 return get(ID_base_name);
196 return set(ID_base_name, base_name);
201 return get(ID_access);
206 return set(ID_access, access);
211 return get(ID_pretty_name);
216 return set(ID_pretty_name, name);
226 return set(ID_anonymous, anonymous);
236 return set(ID_C_is_padding, is_padding);
258 const irep_idt &component_name)
const;
279 assert(type.
id()==ID_struct ||
280 type.
id()==ID_union);
289 assert(type.
id()==ID_struct ||
290 type.
id()==ID_union);
319 assert(type.
id()==ID_struct);
328 assert(type.
id()==ID_struct);
339 set(ID_C_class,
true);
362 return is_class()?ID_private:ID_public;
386 assert(it->id()==ID_base);
388 assert(type.id()==ID_symbol);
389 if(type.get(ID_identifier)==
id)
409 assert(type.
id()==ID_struct);
418 assert(type.
id()==ID_struct);
444 assert(type.
id()==ID_union);
453 assert(type.
id()==ID_union);
476 set(ID_identifier, identifier);
481 return get(ID_identifier);
497 assert(type.
id()==ID_c_enum_tag ||
498 type.
id()==ID_struct_tag ||
499 type.
id()==ID_union_tag);
500 return static_cast<const tag_typet &
>(type);
508 assert(type.
id()==ID_c_enum_tag ||
509 type.
id()==ID_struct_tag ||
510 type.
id()==ID_union_tag);
538 assert(type.
id()==ID_struct_tag);
547 assert(type.
id()==ID_struct_tag);
575 assert(type.
id()==ID_union_tag);
584 assert(type.
id()==ID_union_tag);
621 assert(type.
id()==ID_enumeration);
630 assert(type.
id()==ID_enumeration);
653 set(ID_identifier, identifier);
658 set(ID_base_name, base_name);
682 assert(type.
id()==ID_c_enum);
691 assert(type.
id()==ID_c_enum);
719 assert(type.
id()==ID_c_enum_tag);
728 assert(type.
id()==ID_c_enum_tag);
766 return add_expr(ID_C_default_value);
774 set(ID_C_identifier, identifier);
779 set(ID_C_base_name, name);
784 return get(ID_C_identifier);
789 return get(ID_C_base_name);
799 set(ID_C_this,
true);
811 return !p.empty() && p.front().get_this();
821 add(ID_parameters).
set(ID_ellipsis,
true);
858 set(ID_C_inlined, value);
864 std::vector<irep_idt> result;
866 result.reserve(p.size());
867 for(parameterst::const_iterator it=p.begin();
869 result.push_back(it->get_identifier());
886 assert(type.
id()==ID_code);
895 assert(type.
id()==ID_code);
909 const typet &_subtype,
917 return static_cast<const exprt &
>(
find(ID_size));
922 return static_cast<exprt &
>(
add(ID_size));
948 assert(type.
id()==ID_array);
957 assert(type.
id()==ID_array);
988 assert(type.
id()==ID_array);
997 assert(type.
id()==ID_array);
1017 const typet &_subtype,
1037 set(ID_width, width);
1053 assert(type.
id()==ID_signedbv ||
1054 type.
id()==ID_unsignedbv ||
1055 type.
id()==ID_fixedbv ||
1056 type.
id()==ID_floatbv ||
1057 type.
id()==ID_verilog_signedbv ||
1058 type.
id()==ID_verilog_unsignedbv ||
1060 type.
id()==ID_pointer ||
1061 type.
id()==ID_c_bit_field ||
1062 type.
id()==ID_c_bool);
1069 assert(type.
id()==ID_signedbv ||
1070 type.
id()==ID_unsignedbv ||
1071 type.
id()==ID_fixedbv ||
1072 type.
id()==ID_floatbv ||
1073 type.
id()==ID_verilog_signedbv ||
1074 type.
id()==ID_verilog_unsignedbv ||
1076 type.
id()==ID_pointer ||
1077 type.
id()==ID_c_bit_field ||
1078 type.
id()==ID_c_bool);
1110 assert(type.
id()==ID_bv);
1111 return static_cast<const bv_typet &
>(type);
1119 assert(type.
id()==ID_bv);
1120 return static_cast<bv_typet &
>(type);
1156 assert(type.
id()==ID_unsignedbv);
1165 assert(type.
id()==ID_unsignedbv);
1202 assert(type.
id()==ID_signedbv);
1211 assert(type.
id()==ID_signedbv);
1233 set(ID_integer_bits, b);
1249 assert(type.
id()==ID_fixedbv);
1268 std::size_t
get_f()
const;
1288 assert(type.
id()==ID_floatbv);
1321 assert(type.
id()==ID_c_bit_field);
1337 assert(type.
id()==ID_c_bit_field);
1379 assert(type.
id()==ID_pointer);
1388 assert(type.
id()==ID_pointer);
1399 set(ID_C_reference,
true);
1406 set(ID_C_reference,
true);
1412 set(ID_C_reference,
true);
1428 assert(type.
id()==ID_pointer && type.
get_bool(ID_C_reference));
1437 assert(type.
id()==ID_pointer && type.
get_bool(ID_C_reference));
1475 assert(type.
id()==ID_c_bool);
1484 assert(type.
id()==ID_c_bool);
1510 assert(type.
id()==ID_string);
1548 assert(type.
id()==ID_range);
1562 const typet &_subtype,
1570 return static_cast<const exprt &
>(
find(ID_size));
1575 return static_cast<exprt &
>(
add(ID_size));
1591 assert(type.
id()==ID_vector);
1600 assert(type.
id()==ID_vector);
1631 assert(type.
id()==ID_complex);
1640 assert(type.
id()==ID_complex);
1644 #endif // CPROVER_UTIL_STD_TYPES_H
const irept & get_nil_irep()
const irep_idt & get_name() const
The type of an expression.
std::size_t get_e() const
A generic tag-based type.
c_enum_typet(const typet &_subtype)
Fixed-width bit-vector with unsigned binary interpretation.
constant_exprt zero_expr() const
const irep_idt & get_identifier() const
array_typet(const typet &_subtype, const exprt &_size)
bitvector_typet(const irep_idt &_id, const typet &_subtype, std::size_t width)
bool is_rvalue_reference(const typet &type)
TO_BE_DOCUMENTED.
constant_exprt largest_expr() const
Natural numbers (which include zero)
tag_typet(const irep_idt &_id, const irep_idt &identifier)
c_bool_typet(std::size_t width)
signedbv_typet(std::size_t width)
Fixed-width bit-vector with IEEE floating-point interpretation.
std::vector< irept > subt
irep_idt default_access() const
A generic enumeration type (not to be confused with C enums)
reference_typet(const typet &_subtype, std::size_t _width)
bool has_base(const irep_idt &id) const
bool has_ellipsis() const
const tag_typet & to_tag_type(const typet &type)
Cast a generic typet to a tag_typet.
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
std::size_t get_integer_bits() const
pointer_typet(const typet &_subtype)
Unbounded, signed rational numbers.
std::vector< componentt > componentst
bitvector_typet(const irep_idt &_id, std::size_t width)
std::vector< parametert > parameterst
const componentst & components() const
bool is_incomplete() const
const exprt & find_expr(const irep_idt &name) const
void set_identifier(const irep_idt &identifier)
const memberst & members() const
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
void set_identifier(const irep_idt &identifier)
A constant literal expression.
bool get_bool(const irep_namet &name) const
void set_identifier(const irep_idt &identifier)
unsignedbv_typet(std::size_t width)
bool has_default_value() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
bitvector_typet(const irep_idt &_id)
void set_base_name(const irep_idt &name)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const irep_idt & get_base_name() const
c_bit_field_typet(const typet &subtype, std::size_t width)
struct_union_typet(const irep_idt &_id)
mp_integer get_to() const
reference_typet(const typet &_subtype)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void set_is_padding(bool is_padding)
const irep_idt & get_base_name() const
std::vector< irep_idt > parameter_identifiers() const
void set_inlined(bool value)
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
const methodst & methods() const
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
void set_value(const irep_idt &value)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
constant_exprt smallest_expr() const
A reference into the symbol table.
irep_idt get_identifier() const
symbol_typet(const irep_idt &identifier)
std::size_t get_fraction_bits() const
void set_access(const irep_idt &access)
Fixed-width bit-vector with two's complement interpretation.
A constant-size array type.
void set_integer_bits(std::size_t b)
componentst & components()
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
range_typet(const mp_integer &_from, const mp_integer &_to)
const exprt & size() const
vector_typet(const typet &_subtype, const exprt &_size)
void set_tag(const irep_idt &tag)
mp_integer smallest() const
const exprt & size() const
Base class for tree-like data structures with sharing.
const string_typet & to_string_type(const typet &type)
Cast a generic typet to a string_typet.
void set_from(const mp_integer &_from)
signedbv_typet difference_type() const
bv_typet(std::size_t width)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
mp_integer largest() const
mp_integer smallest() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
pointer_typet(const typet &_subtype, std::size_t width)
complex_typet(const typet &_subtype)
typet component_type(const irep_idt &component_name) const
Fixed-width bit-vector with signed fixed-point interpretation.
Base class of bitvector types.
const irept::subt & elements() const
std::size_t get_width() const
tag_typet(const irep_idt &_id)
const irep_idt & get_pretty_name() const
bool has_component(const irep_idt &component_name) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
std::size_t get_f() const
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Unbounded, signed integers.
Complex numbers made of pair of given subtype.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
void set_identifier(const irep_idt &identifier)
mp_integer largest() const
bool is_prefix_of(const struct_typet &other) const
bitvector_typet(const irep_idt &_id, const typet &_subtype)
constant_exprt largest_expr() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const irep_idt & get_access() const
Base type of C structs and unions, and C++ classes.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Unbounded, signed real numbers.
bool get_anonymous() const
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Base class for all expressions.
const typet & find_type(const irep_namet &name) const
const parameterst & parameters() const
std::size_t component_number(const irep_idt &component_name) const
void set_pretty_name(const irep_idt &name)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
A type for subranges of integers.
constant_exprt smallest_expr() const
irept & add(const irep_namet &name)
typet & add_type(const irep_namet &name)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
incomplete_array_typet(const typet &_subtype)
void set_f(std::size_t b)
bool get_is_padding() const
void set_anonymous(bool anonymous)
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
const irept::subt & bases() const
struct_tag_typet(const irep_idt &identifier)
exprt & add_expr(const irep_idt &name)
void remove(const irep_namet &name)
const typet & subtype() const
parametert(const typet &type)
parameterst & parameters()
void set_to(const mp_integer &to)
fixed-width bit-vector without numerical interpretation
std::size_t get_size_t(const irep_namet &name) const
irep_idt get_base_name() const
c_enum_tag_typet(const irep_idt &identifier)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
const irep_idt & get_identifier() const
std::vector< c_enum_membert > memberst
const irept & find(const irep_namet &name) const
const typet & return_type() const
const irep_idt & get_identifier() const
void set_base_name(const irep_idt &base_name)
void add_base(const typet &base)
const exprt & default_value() const
void set(const irep_namet &name, const irep_idt &value)
componentt(const irep_idt &_name, const typet &_type)
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
const componentt & get_component(const irep_idt &component_name) const
union_tag_typet(const irep_idt &identifier)
void set_width(std::size_t width)
irep_idt get_value() const
#define forall_irep(it, irep)
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
constant_exprt zero_expr() const
mp_integer get_from() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.