9 #ifndef CPROVER_UTIL_STD_TYPES_H 10 #define CPROVER_UTIL_STD_TYPES_H 24 #include <unordered_map> 120 set(ID_identifier, identifier);
125 return get(ID_identifier);
157 return type.id() == ID_symbol;
189 return set(ID_name, name);
194 return get(ID_base_name);
199 return set(ID_base_name, base_name);
204 return get(ID_access);
209 return set(ID_access, access);
214 return get(ID_pretty_name);
219 return set(ID_pretty_name, name);
229 return set(ID_anonymous, anonymous);
239 return set(ID_C_is_padding, is_padding);
261 const irep_idt &component_name)
const;
336 return type.id() == ID_struct;
346 set(ID_C_class,
true);
369 return is_class()?ID_private:ID_public;
406 for(
const auto &b :
bases())
506 set(ID_identifier, identifier);
511 return get(ID_identifier);
528 type.
id()==ID_struct_tag ||
529 type.
id()==ID_union_tag);
530 return static_cast<const tag_typet &
>(type);
539 type.
id()==ID_struct_tag ||
540 type.
id()==ID_union_tag);
683 set(ID_identifier, identifier);
688 set(ID_base_name, base_name);
790 DEPRECATED(
"Use the two argument constructor instead")
824 return add_expr(ID_C_default_value);
832 set(ID_C_identifier, identifier);
837 set(ID_C_base_name, name);
842 return get(ID_C_identifier);
847 return get(ID_C_base_name);
857 set(ID_C_this,
true);
874 if(!p.empty() && p.front().get_this())
887 add(ID_parameters).
set(ID_ellipsis,
true);
922 set(ID_C_inlined, value);
927 return get(ID_access);
932 return set(ID_access, access);
942 set(ID_constructor,
true);
948 std::vector<irep_idt> result;
950 result.reserve(p.size());
951 for(parameterst::const_iterator it=p.begin();
953 result.push_back(it->get_identifier());
965 std::size_t index = 0;
968 const irep_idt &
id = p.get_identifier();
1008 const typet &_subtype,
1016 return static_cast<const exprt &
>(
find(ID_size));
1021 return static_cast<exprt &
>(
add(ID_size));
1116 const typet &_subtype,
1136 set(ID_width, width);
1153 type.
id()==ID_unsignedbv ||
1154 type.
id()==ID_fixedbv ||
1155 type.
id()==ID_floatbv ||
1156 type.
id()==ID_verilog_signedbv ||
1157 type.
id()==ID_verilog_unsignedbv ||
1159 type.
id()==ID_pointer ||
1160 type.
id()==ID_c_bit_field ||
1161 type.
id()==ID_c_bool);
1169 type.
id()==ID_unsignedbv ||
1170 type.
id()==ID_fixedbv ||
1171 type.
id()==ID_floatbv ||
1172 type.
id()==ID_verilog_signedbv ||
1173 type.
id()==ID_verilog_unsignedbv ||
1175 type.
id()==ID_pointer ||
1176 type.
id()==ID_c_bit_field ||
1177 type.
id()==ID_c_bool);
1206 return static_cast<const bv_typet &
>(type);
1215 return static_cast<bv_typet &
>(type);
1320 set(ID_integer_bits, b);
1355 std::size_t
get_f()
const;
1472 return type.id() == ID_pointer;
1489 set(ID_C_reference,
true);
1633 const typet &_subtype,
1641 return static_cast<const exprt &
>(
find(ID_size));
1646 return static_cast<exprt &
>(
add(ID_size));
1729 return get(ID_identifier);
1734 return set(ID_identifier, identifier);
1739 return static_cast<typet &
>(
add(ID_type));
1744 return static_cast<const typet &
>(
find(ID_type));
1751 :
typet(ID_mathematical_function)
1815 #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
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
A generic tag-based type.
c_enum_typet(const typet &_subtype)
Fixed-width bit-vector with unsigned binary interpretation.
constant_exprt zero_expr() const
void set_access(const irep_idt &access)
code_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
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)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
std::vector< baset > basest
tag_typet(const irep_idt &_id, const irep_idt &identifier)
c_bool_typet(std::size_t width)
signedbv_typet(std::size_t width)
void validate_type(const pointer_typet &type)
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
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 code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
std::size_t get_integer_bits() const
const tag_typet & to_tag_type(const typet &type)
Cast a generic typet to a tag_typet.
Unbounded, signed rational numbers.
std::vector< componentt > componentst
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
bitvector_typet(const irep_idt &_id, std::size_t width)
std::vector< parametert > parameterst
const typet & type() const
std::vector< variablet > domaint
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
void set_identifier(const irep_idt &identifier)
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
A constant literal expression.
bool get_is_constructor() const
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
bitvector_typet(const irep_idt &_id)
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
void set_base_name(const irep_idt &name)
bool can_cast_type< pointer_typet >(const typet &type)
Templated functions to cast to specific exprt-derived classes.
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)
void set_is_constructor()
irep_idt get_identifier() const
bool can_cast_type< struct_typet >(const typet &type)
mp_integer get_to() const
const irep_idt & id() const
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 methodst & methods() const
void set_value(const irep_idt &value)
constant_exprt smallest_expr() const
A reference into the symbol table.
A type for mathematical functions (do not confuse with functions/methods in code) ...
irep_idt get_identifier() const
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
std::unordered_map< irep_idt, std::size_t > parameter_indicest
symbol_typet(const irep_idt &identifier)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
std::size_t get_fraction_bits() const
void set_access(const irep_idt &access)
Fixed-width bit-vector with two's complement interpretation.
const parametert * get_this() const
void set_identifier(const irep_idt &identifier)
A constant-size array type.
nonstd::optional< T > optionalt
void set_integer_bits(std::size_t b)
componentst & components()
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
const irep_idt & get(const irep_namet &name) const
range_typet(const mp_integer &_from, const mp_integer &_to)
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
const exprt & size() const
#define PRECONDITION(CONDITION)
vector_typet(const typet &_subtype, const exprt &_size)
void set_tag(const irep_idt &tag)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
mp_integer smallest() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const exprt & size() const
Base class for tree-like data structures with sharing.
const domaint & domain() const
void set_from(const mp_integer &_from)
signedbv_typet difference_type() const
bv_typet(std::size_t width)
mp_integer largest() const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
mp_integer smallest() const
variablet & add_variable()
const irep_idt & get_access() const
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.
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Base class of bitvector types.
const irept::subt & elements() const
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
const irep_idt & get_pretty_name() const
bool has_component(const irep_idt &component_name) const
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
std::size_t get_f() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Unbounded, signed integers.
Complex numbers made of pair of given subtype.
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 irep_idt & get_access() const
Base type of C structs and unions, and C++ classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Unbounded, signed real numbers.
bool get_anonymous() const
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_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
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
void set_pretty_name(const irep_idt &name)
A type for subranges of integers.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
constant_exprt smallest_expr() const
const basest & bases() const
irept & add(const irep_namet &name)
typet & add_type(const irep_namet &name)
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
incomplete_array_typet(const typet &_subtype)
void set_f(std::size_t b)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
const string_typet & to_string_type(const typet &type)
Cast a generic typet to a string_typet.
bool get_is_padding() const
void set_anonymous(bool anonymous)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
struct_tag_typet(const irep_idt &identifier)
exprt & add_expr(const irep_idt &name)
void remove(const irep_namet &name)
const typet & subtype() const
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.
#define DATA_INVARIANT(CONDITION, REASON)
parametert(const typet &type)
parameterst & parameters()
void set_to(const mp_integer &to)
fixed-width bit-vector without numerical interpretation
const typet & codomain() const
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)
code_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
const irep_idt & get_identifier() const
std::vector< c_enum_membert > memberst
const irept & find(const irep_namet &name) const
bool can_cast_type< class_typet >(const typet &type)
const typet & return_type() const
bool can_cast_type< symbol_typet >(const typet &type)
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 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
constant_exprt zero_expr() const
mp_integer get_from() const