cprover
std_types.h File Reference

Pre-defined types. More...

#include "expr.h"
#include "expr_cast.h"
#include "invariant.h"
#include "mp_arith.h"
#include "validate.h"
#include <unordered_map>
+ Include dependency graph for std_types.h:

Go to the source code of this file.

Classes

class  bool_typet
 The Boolean type. More...
 
class  nil_typet
 The NIL type, i.e., an invalid type, no value. More...
 
class  empty_typet
 The empty type. More...
 
class  void_typet
 The void type, the same as empty_typet. More...
 
class  symbol_typet
 A reference into the symbol table. More...
 
class  struct_union_typet
 Base type for structs and unions. More...
 
class  struct_union_typet::componentt
 
class  struct_typet
 Structure type, corresponds to C style structs. More...
 
class  struct_typet::baset
 Base class or struct that a class or struct inherits from. More...
 
class  class_typet
 Class type. More...
 
class  union_typet
 The union type. More...
 
class  tag_typet
 A tag-based type, i.e., typet with an identifier. More...
 
class  struct_tag_typet
 A struct tag type, i.e., struct_typet with an identifier. More...
 
class  union_tag_typet
 A union tag type, i.e., union_typet with an identifier. More...
 
class  enumeration_typet
 An enumeration type, i.e., a type with elements (not to be confused with C enums) More...
 
class  c_enum_typet
 The type of C enums. More...
 
class  c_enum_typet::c_enum_membert
 
class  c_enum_tag_typet
 C enum tag type, i.e., c_enum_typet with an identifier. More...
 
class  code_typet
 Base type of functions. More...
 
class  code_typet::parametert
 
class  array_typet
 Arrays with given size. More...
 
class  incomplete_array_typet
 Arrays without size. More...
 
class  bitvector_typet
 Base class of fixed-width bit-vector types. More...
 
class  bv_typet
 Fixed-width bit-vector without numerical interpretation. More...
 
class  unsignedbv_typet
 Fixed-width bit-vector with unsigned binary interpretation. More...
 
class  signedbv_typet
 Fixed-width bit-vector with two's complement interpretation. More...
 
class  fixedbv_typet
 Fixed-width bit-vector with signed fixed-point interpretation. More...
 
class  floatbv_typet
 Fixed-width bit-vector with IEEE floating-point interpretation. More...
 
class  c_bit_field_typet
 Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More...
 
class  pointer_typet
 The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More...
 
class  reference_typet
 The reference type. More...
 
class  c_bool_typet
 The C/C++ Booleans. More...
 
class  string_typet
 String type. More...
 
class  range_typet
 A type for subranges of integers. More...
 
class  vector_typet
 The vector type. More...
 
class  complex_typet
 Complex numbers made of pair of given subtype. More...
 

Functions

template<>
bool can_cast_type< symbol_typet > (const typet &type)
 Check whether a reference to a typet is a symbol_typet. More...
 
const symbol_typetto_symbol_type (const typet &type)
 Cast a typet to a symbol_typet. More...
 
symbol_typetto_symbol_type (typet &type)
 Cast a typet to a symbol_typet. More...
 
template<>
bool can_cast_type< struct_union_typet > (const typet &type)
 Check whether a reference to a typet is a struct_union_typet. More...
 
const struct_union_typetto_struct_union_type (const typet &type)
 Cast a typet to a struct_union_typet. More...
 
struct_union_typetto_struct_union_type (typet &type)
 Cast a typet to a struct_union_typet. More...
 
template<>
bool can_cast_type< struct_typet > (const typet &type)
 Check whether a reference to a typet is a struct_typet. More...
 
const struct_typetto_struct_type (const typet &type)
 Cast a typet to a struct_typet. More...
 
struct_typetto_struct_type (typet &type)
 Cast a typet to a struct_typet. More...
 
template<>
bool can_cast_type< class_typet > (const typet &type)
 Check whether a reference to a typet is a class_typet. More...
 
const class_typetto_class_type (const typet &type)
 Cast a typet to a class_typet. More...
 
class_typetto_class_type (typet &type)
 Cast a typet to a class_typet. More...
 
template<>
bool can_cast_type< union_typet > (const typet &type)
 Check whether a reference to a typet is a union_typet. More...
 
const union_typetto_union_type (const typet &type)
 Cast a typet to a union_typet. More...
 
union_typetto_union_type (typet &type)
 Cast a typet to a union_typet. More...
 
template<>
bool can_cast_type< tag_typet > (const typet &type)
 Check whether a reference to a typet is a tag_typet. More...
 
const tag_typetto_tag_type (const typet &type)
 Cast a typet to a tag_typet. More...
 
tag_typetto_tag_type (typet &type)
 Cast a typet to a tag_typet. More...
 
template<>
bool can_cast_type< struct_tag_typet > (const typet &type)
 Check whether a reference to a typet is a struct_tag_typet. More...
 
const struct_tag_typetto_struct_tag_type (const typet &type)
 Cast a typet to a struct_tag_typet. More...
 
struct_tag_typetto_struct_tag_type (typet &type)
 Cast a typet to a struct_tag_typet. More...
 
template<>
bool can_cast_type< union_tag_typet > (const typet &type)
 Check whether a reference to a typet is a union_tag_typet. More...
 
const union_tag_typetto_union_tag_type (const typet &type)
 Cast a typet to a union_tag_typet. More...
 
union_tag_typetto_union_tag_type (typet &type)
 Cast a typet to a union_tag_typet. More...
 
template<>
bool can_cast_type< enumeration_typet > (const typet &type)
 Check whether a reference to a typet is a enumeration_typet. More...
 
const enumeration_typetto_enumeration_type (const typet &type)
 Cast a typet to a enumeration_typet. More...
 
enumeration_typetto_enumeration_type (typet &type)
 Cast a typet to a enumeration_typet. More...
 
template<>
bool can_cast_type< c_enum_typet > (const typet &type)
 Check whether a reference to a typet is a c_enum_typet. More...
 
const c_enum_typetto_c_enum_type (const typet &type)
 Cast a typet to a c_enum_typet. More...
 
c_enum_typetto_c_enum_type (typet &type)
 Cast a typet to a c_enum_typet. More...
 
template<>
bool can_cast_type< c_enum_tag_typet > (const typet &type)
 Check whether a reference to a typet is a c_enum_tag_typet. More...
 
const c_enum_tag_typetto_c_enum_tag_type (const typet &type)
 Cast a typet to a c_enum_tag_typet. More...
 
c_enum_tag_typetto_c_enum_tag_type (typet &type)
 Cast a typet to a c_enum_tag_typet. More...
 
template<>
bool can_cast_type< code_typet > (const typet &type)
 Check whether a reference to a typet is a code_typet. More...
 
const code_typetto_code_type (const typet &type)
 Cast a typet to a code_typet. More...
 
code_typetto_code_type (typet &type)
 Cast a typet to a code_typet. More...
 
template<>
bool can_cast_type< array_typet > (const typet &type)
 Check whether a reference to a typet is a array_typet. More...
 
const array_typetto_array_type (const typet &type)
 Cast a typet to an array_typet. More...
 
array_typetto_array_type (typet &type)
 Cast a typet to an array_typet. More...
 
template<>
bool can_cast_type< incomplete_array_typet > (const typet &type)
 Check whether a reference to a typet is a incomplete_array_typet. More...
 
const incomplete_array_typetto_incomplete_array_type (const typet &type)
 Cast a typet to an incomplete_array_typet. More...
 
incomplete_array_typetto_incomplete_array_type (typet &type)
 Cast a typet to an incomplete_array_typet. More...
 
template<>
bool can_cast_type< bitvector_typet > (const typet &type)
 Check whether a reference to a typet is a bitvector_typet. More...
 
const bitvector_typetto_bitvector_type (const typet &type)
 Cast a typet to a bitvector_typet. More...
 
bitvector_typetto_bitvector_type (typet &type)
 Cast a typet to a bitvector_typet. More...
 
template<>
bool can_cast_type< bv_typet > (const typet &type)
 Check whether a reference to a typet is a bv_typet. More...
 
void validate_type (const bv_typet &type)
 
const bv_typetto_bv_type (const typet &type)
 Cast a typet to a bv_typet. More...
 
bv_typetto_bv_type (typet &type)
 Cast a typet to a bv_typet. More...
 
template<>
bool can_cast_type< unsignedbv_typet > (const typet &type)
 Check whether a reference to a typet is a unsignedbv_typet. More...
 
const unsignedbv_typetto_unsignedbv_type (const typet &type)
 Cast a typet to an unsignedbv_typet. More...
 
unsignedbv_typetto_unsignedbv_type (typet &type)
 Cast a typet to an unsignedbv_typet. More...
 
template<>
bool can_cast_type< signedbv_typet > (const typet &type)
 Check whether a reference to a typet is a signedbv_typet. More...
 
void validate_type (const signedbv_typet &type)
 
const signedbv_typetto_signedbv_type (const typet &type)
 Cast a typet to a signedbv_typet. More...
 
signedbv_typetto_signedbv_type (typet &type)
 Cast a typet to a signedbv_typet. More...
 
template<>
bool can_cast_type< fixedbv_typet > (const typet &type)
 Check whether a reference to a typet is a fixedbv_typet. More...
 
void validate_type (const fixedbv_typet &type)
 
const fixedbv_typetto_fixedbv_type (const typet &type)
 Cast a typet to a fixedbv_typet. More...
 
fixedbv_typetto_fixedbv_type (typet &type)
 Cast a typet to a fixedbv_typet. More...
 
template<>
bool can_cast_type< floatbv_typet > (const typet &type)
 Check whether a reference to a typet is a floatbv_typet. More...
 
void validate_type (const floatbv_typet &type)
 
const floatbv_typetto_floatbv_type (const typet &type)
 Cast a typet to a floatbv_typet. More...
 
floatbv_typetto_floatbv_type (typet &type)
 Cast a typet to a floatbv_typet. More...
 
template<>
bool can_cast_type< c_bit_field_typet > (const typet &type)
 Check whether a reference to a typet is a c_bit_field_typet. More...
 
const c_bit_field_typetto_c_bit_field_type (const typet &type)
 Cast a typet to a c_bit_field_typet. More...
 
c_bit_field_typetto_c_bit_field_type (typet &type)
 Cast a typet to a c_bit_field_typet. More...
 
template<>
bool can_cast_type< pointer_typet > (const typet &type)
 Check whether a reference to a typet is a pointer_typet. More...
 
void validate_type (const pointer_typet &type)
 
const pointer_typetto_pointer_type (const typet &type)
 Cast a typet to a pointer_typet. More...
 
pointer_typetto_pointer_type (typet &type)
 Cast a typet to a pointer_typet. More...
 
template<>
bool can_cast_type< reference_typet > (const typet &type)
 Check whether a reference to a typet is a reference_typet. More...
 
const reference_typetto_reference_type (const typet &type)
 Cast a typet to a reference_typet. More...
 
reference_typetto_reference_type (typet &type)
 Cast a typet to a reference_typet. More...
 
bool is_reference (const typet &type)
 Returns true if the type is a reference. More...
 
bool is_rvalue_reference (const typet &type)
 Returns if the type is an R value reference. More...
 
template<>
bool can_cast_type< c_bool_typet > (const typet &type)
 Check whether a reference to a typet is a c_bool_typet. More...
 
void validate_type (const c_bool_typet &type)
 
const c_bool_typetto_c_bool_type (const typet &type)
 Cast a typet to a c_bool_typet. More...
 
c_bool_typetto_c_bool_type (typet &type)
 Cast a typet to a c_bool_typet. More...
 
template<>
bool can_cast_type< string_typet > (const typet &type)
 Check whether a reference to a typet is a string_typet. More...
 
const string_typetto_string_type (const typet &type)
 Cast a typet to a string_typet. More...
 
string_typetto_string_type (typet &type)
 Cast a typet to a string_typet. More...
 
template<>
bool can_cast_type< range_typet > (const typet &type)
 Check whether a reference to a typet is a range_typet. More...
 
const range_typetto_range_type (const typet &type)
 Cast a typet to a range_typet. More...
 
range_typetto_range_type (typet &type)
 Cast a typet to a range_typet. More...
 
template<>
bool can_cast_type< vector_typet > (const typet &type)
 Check whether a reference to a typet is a vector_typet. More...
 
const vector_typetto_vector_type (const typet &type)
 Cast a typet to a vector_typet. More...
 
vector_typetto_vector_type (typet &type)
 Cast a typet to a vector_typet. More...
 
template<>
bool can_cast_type< complex_typet > (const typet &type)
 Check whether a reference to a typet is a complex_typet. More...
 
const complex_typetto_complex_type (const typet &type)
 Cast a typet to a complex_typet. More...
 
complex_typetto_complex_type (typet &type)
 Cast a typet to a complex_typet. More...
 
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. More...
 

Detailed Description

Pre-defined types.

Definition in file std_types.h.

Function Documentation

◆ can_cast_type< array_typet >()

template<>
bool can_cast_type< array_typet > ( const typet type)
inline

Check whether a reference to a typet is a array_typet.

Parameters
typeSource type.
Returns
True if type is a array_typet.

Definition at line 1056 of file std_types.h.

◆ can_cast_type< bitvector_typet >()

template<>
bool can_cast_type< bitvector_typet > ( const typet type)
inline

Check whether a reference to a typet is a bitvector_typet.

Parameters
typeSource type.
Returns
True if type is a bitvector_typet.

Definition at line 1160 of file std_types.h.

◆ can_cast_type< bv_typet >()

template<>
bool can_cast_type< bv_typet > ( const typet type)
inline

Check whether a reference to a typet is a bv_typet.

Parameters
typeSource type.
Returns
True if type is a bv_typet.

Definition at line 1207 of file std_types.h.

◆ can_cast_type< c_bit_field_typet >()

template<>
bool can_cast_type< c_bit_field_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_bit_field_typet.

Parameters
typeSource type.
Returns
True if type is a c_bit_field_typet.

Definition at line 1498 of file std_types.h.

◆ can_cast_type< c_bool_typet >()

template<>
bool can_cast_type< c_bool_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_bool_typet.

Parameters
typeSource type.
Returns
True if type is a c_bool_typet.

Definition at line 1644 of file std_types.h.

◆ can_cast_type< c_enum_tag_typet >()

template<>
bool can_cast_type< c_enum_tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_enum_tag_typet.

Parameters
typeSource type.
Returns
True if type is a c_enum_tag_typet.

Definition at line 745 of file std_types.h.

◆ can_cast_type< c_enum_typet >()

template<>
bool can_cast_type< c_enum_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_enum_typet.

Parameters
typeSource type.
Returns
True if type is a c_enum_typet.

Definition at line 705 of file std_types.h.

◆ can_cast_type< class_typet >()

template<>
bool can_cast_type< class_typet > ( const typet type)
inline

Check whether a reference to a typet is a class_typet.

Parameters
typeSource type.
Returns
True if type is a class_typet.

Definition at line 417 of file std_types.h.

◆ can_cast_type< code_typet >()

template<>
bool can_cast_type< code_typet > ( const typet type)
inline

Check whether a reference to a typet is a code_typet.

Parameters
typeSource type.
Returns
True if type is a code_typet.

Definition at line 990 of file std_types.h.

◆ can_cast_type< complex_typet >()

template<>
bool can_cast_type< complex_typet > ( const typet type)
inline

Check whether a reference to a typet is a complex_typet.

Parameters
typeSource type.
Returns
True if type is a complex_typet.

Definition at line 1844 of file std_types.h.

◆ can_cast_type< enumeration_typet >()

template<>
bool can_cast_type< enumeration_typet > ( const typet type)
inline

Check whether a reference to a typet is a enumeration_typet.

Parameters
typeSource type.
Returns
True if type is a enumeration_typet.

Definition at line 641 of file std_types.h.

◆ can_cast_type< fixedbv_typet >()

template<>
bool can_cast_type< fixedbv_typet > ( const typet type)
inline

Check whether a reference to a typet is a fixedbv_typet.

Parameters
typeSource type.
Returns
True if type is a fixedbv_typet.

Definition at line 1381 of file std_types.h.

◆ can_cast_type< floatbv_typet >()

template<>
bool can_cast_type< floatbv_typet > ( const typet type)
inline

Check whether a reference to a typet is a floatbv_typet.

Parameters
typeSource type.
Returns
True if type is a floatbv_typet.

Definition at line 1443 of file std_types.h.

◆ can_cast_type< incomplete_array_typet >()

template<>
bool can_cast_type< incomplete_array_typet > ( const typet type)
inline

Check whether a reference to a typet is a incomplete_array_typet.

Parameters
typeSource type.
Returns
True if type is a incomplete_array_typet.

Definition at line 1095 of file std_types.h.

◆ can_cast_type< pointer_typet >()

template<>
bool can_cast_type< pointer_typet > ( const typet type)
inline

Check whether a reference to a typet is a pointer_typet.

Parameters
typeSource type.
Returns
True if type is a pointer_typet.

Definition at line 1546 of file std_types.h.

◆ can_cast_type< range_typet >()

template<>
bool can_cast_type< range_typet > ( const typet type)
inline

Check whether a reference to a typet is a range_typet.

Parameters
typeSource type.
Returns
True if type is a range_typet.

Definition at line 1741 of file std_types.h.

◆ can_cast_type< reference_typet >()

template<>
bool can_cast_type< reference_typet > ( const typet type)
inline

Check whether a reference to a typet is a reference_typet.

Parameters
typeSource type.
Returns
True if type is a reference_typet.

Definition at line 1599 of file std_types.h.

◆ can_cast_type< signedbv_typet >()

template<>
bool can_cast_type< signedbv_typet > ( const typet type)
inline

Check whether a reference to a typet is a signedbv_typet.

Parameters
typeSource type.
Returns
True if type is a signedbv_typet.

Definition at line 1317 of file std_types.h.

◆ can_cast_type< string_typet >()

template<>
bool can_cast_type< string_typet > ( const typet type)
inline

Check whether a reference to a typet is a string_typet.

Parameters
typeSource type.
Returns
True if type is a string_typet.

Definition at line 1694 of file std_types.h.

◆ can_cast_type< struct_tag_typet >()

template<>
bool can_cast_type< struct_tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a struct_tag_typet.

Parameters
typeSource type.
Returns
True if type is a struct_tag_typet.

Definition at line 551 of file std_types.h.

◆ can_cast_type< struct_typet >()

template<>
bool can_cast_type< struct_typet > ( const typet type)
inline

Check whether a reference to a typet is a struct_typet.

Parameters
typeSource type.
Returns
True if type is a struct_typet.

Definition at line 357 of file std_types.h.

◆ can_cast_type< struct_union_typet >()

template<>
bool can_cast_type< struct_union_typet > ( const typet type)
inline

Check whether a reference to a typet is a struct_union_typet.

Parameters
typeSource type.
Returns
True if type is a struct_union_typet.

Definition at line 249 of file std_types.h.

◆ can_cast_type< symbol_typet >()

template<>
bool can_cast_type< symbol_typet > ( const typet type)
inline

Check whether a reference to a typet is a symbol_typet.

Parameters
typeSource type.
Returns
True if type is a symbol_typet.

Definition at line 85 of file std_types.h.

◆ can_cast_type< tag_typet >()

template<>
bool can_cast_type< tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a tag_typet.

Parameters
typeSource type.
Returns
True if type is a tag_typet.

Definition at line 510 of file std_types.h.

◆ can_cast_type< union_tag_typet >()

template<>
bool can_cast_type< union_tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a union_tag_typet.

Parameters
typeSource type.
Returns
True if type is a union_tag_typet.

Definition at line 591 of file std_types.h.

◆ can_cast_type< union_typet >()

template<>
bool can_cast_type< union_typet > ( const typet type)
inline

Check whether a reference to a typet is a union_typet.

Parameters
typeSource type.
Returns
True if type is a union_typet.

Definition at line 458 of file std_types.h.

◆ can_cast_type< unsignedbv_typet >()

template<>
bool can_cast_type< unsignedbv_typet > ( const typet type)
inline

Check whether a reference to a typet is a unsignedbv_typet.

Parameters
typeSource type.
Returns
True if type is a unsignedbv_typet.

Definition at line 1269 of file std_types.h.

◆ can_cast_type< vector_typet >()

template<>
bool can_cast_type< vector_typet > ( const typet type)
inline

Check whether a reference to a typet is a vector_typet.

Parameters
typeSource type.
Returns
True if type is a vector_typet.

Definition at line 1800 of file std_types.h.

◆ is_constant_or_has_constant_components()

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.

Examples include:

  • const int a;
  • struct contains_constant_pointer { int x; int * const p; };
  • const int b[3];
    Parameters
    typeThe type we want to query constness of.
    nsThe namespace, needed for resolution of symbols.
    Returns
    Whether passed in type is const or not.

Definition at line 195 of file std_types.cpp.

◆ is_reference()

bool is_reference ( const typet type)

Returns true if the type is a reference.

Definition at line 103 of file std_types.cpp.

◆ is_rvalue_reference()

bool is_rvalue_reference ( const typet type)

Returns if the type is an R value reference.

Definition at line 110 of file std_types.cpp.

◆ to_array_type() [1/2]

const array_typet& to_array_type ( const typet type)
inline

Cast a typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type array_typet.

Definition at line 1069 of file std_types.h.

◆ to_array_type() [2/2]

array_typet& to_array_type ( typet type)
inline

Cast a typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type array_typet.

Definition at line 1076 of file std_types.h.

◆ to_bitvector_type() [1/2]

const bitvector_typet& to_bitvector_type ( const typet type)
inline

Cast a typet to a bitvector_typet.

This is an unchecked conversion. type must be known to be bitvector_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type bitvector_typet.

Definition at line 1178 of file std_types.h.

◆ to_bitvector_type() [2/2]

bitvector_typet& to_bitvector_type ( typet type)
inline

Cast a typet to a bitvector_typet.

This is an unchecked conversion. type must be known to be bitvector_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type bitvector_typet.

Definition at line 1186 of file std_types.h.

◆ to_bv_type() [1/2]

const bv_typet& to_bv_type ( const typet type)
inline

Cast a typet to a bv_typet.

This is an unchecked conversion. type must be known to be bv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type bv_typet.

Definition at line 1225 of file std_types.h.

◆ to_bv_type() [2/2]

bv_typet& to_bv_type ( typet type)
inline

Cast a typet to a bv_typet.

This is an unchecked conversion. type must be known to be bv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type bv_typet.

Definition at line 1234 of file std_types.h.

◆ to_c_bit_field_type() [1/2]

const c_bit_field_typet& to_c_bit_field_type ( const typet type)
inline

Cast a typet to a c_bit_field_typet.

This is an unchecked conversion. type must be known to be c_bit_field_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_bit_field_typet.

Definition at line 1511 of file std_types.h.

◆ to_c_bit_field_type() [2/2]

c_bit_field_typet& to_c_bit_field_type ( typet type)
inline

Cast a typet to a c_bit_field_typet.

This is an unchecked conversion. type must be known to be c_bit_field_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_bit_field_typet.

Definition at line 1518 of file std_types.h.

◆ to_c_bool_type() [1/2]

const c_bool_typet& to_c_bool_type ( const typet type)
inline

Cast a typet to a c_bool_typet.

This is an unchecked conversion. type must be known to be c_bool_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_bool_typet.

Definition at line 1662 of file std_types.h.

◆ to_c_bool_type() [2/2]

c_bool_typet& to_c_bool_type ( typet type)
inline

Cast a typet to a c_bool_typet.

This is an unchecked conversion. type must be known to be c_bool_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_bool_typet.

Definition at line 1671 of file std_types.h.

◆ to_c_enum_tag_type() [1/2]

const c_enum_tag_typet& to_c_enum_tag_type ( const typet type)
inline

Cast a typet to a c_enum_tag_typet.

This is an unchecked conversion. type must be known to be c_enum_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_enum_tag_typet.

Definition at line 758 of file std_types.h.

◆ to_c_enum_tag_type() [2/2]

c_enum_tag_typet& to_c_enum_tag_type ( typet type)
inline

Cast a typet to a c_enum_tag_typet.

This is an unchecked conversion. type must be known to be c_enum_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_enum_tag_typet.

Definition at line 765 of file std_types.h.

◆ to_c_enum_type() [1/2]

const c_enum_typet& to_c_enum_type ( const typet type)
inline

Cast a typet to a c_enum_typet.

This is an unchecked conversion. type must be known to be c_enum_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_enum_typet.

Definition at line 718 of file std_types.h.

◆ to_c_enum_type() [2/2]

c_enum_typet& to_c_enum_type ( typet type)
inline

Cast a typet to a c_enum_typet.

This is an unchecked conversion. type must be known to be c_enum_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type c_enum_typet.

Definition at line 725 of file std_types.h.

◆ to_class_type() [1/2]

const class_typet& to_class_type ( const typet type)
inline

Cast a typet to a class_typet.

This is an unchecked conversion. type must be known to be class_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type class_typet.

Definition at line 430 of file std_types.h.

◆ to_class_type() [2/2]

class_typet& to_class_type ( typet type)
inline

Cast a typet to a class_typet.

This is an unchecked conversion. type must be known to be class_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type class_typet.

Definition at line 437 of file std_types.h.

◆ to_code_type() [1/2]

const code_typet& to_code_type ( const typet type)
inline

Cast a typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type code_typet.

Definition at line 1003 of file std_types.h.

◆ to_code_type() [2/2]

code_typet& to_code_type ( typet type)
inline

Cast a typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type code_typet.

Definition at line 1011 of file std_types.h.

◆ to_complex_type() [1/2]

const complex_typet& to_complex_type ( const typet type)
inline

Cast a typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type complex_typet.

Definition at line 1857 of file std_types.h.

◆ to_complex_type() [2/2]

complex_typet& to_complex_type ( typet type)
inline

Cast a typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type complex_typet.

Definition at line 1864 of file std_types.h.

◆ to_enumeration_type() [1/2]

const enumeration_typet& to_enumeration_type ( const typet type)
inline

Cast a typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type enumeration_typet.

Definition at line 654 of file std_types.h.

◆ to_enumeration_type() [2/2]

enumeration_typet& to_enumeration_type ( typet type)
inline

Cast a typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type enumeration_typet.

Definition at line 661 of file std_types.h.

◆ to_fixedbv_type() [1/2]

const fixedbv_typet& to_fixedbv_type ( const typet type)
inline

Cast a typet to a fixedbv_typet.

This is an unchecked conversion. type must be known to be fixedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type fixedbv_typet.

Definition at line 1400 of file std_types.h.

◆ to_fixedbv_type() [2/2]

fixedbv_typet& to_fixedbv_type ( typet type)
inline

Cast a typet to a fixedbv_typet.

This is an unchecked conversion. type must be known to be fixedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type fixedbv_typet.

Definition at line 1409 of file std_types.h.

◆ to_floatbv_type() [1/2]

const floatbv_typet& to_floatbv_type ( const typet type)
inline

Cast a typet to a floatbv_typet.

This is an unchecked conversion. type must be known to be floatbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type floatbv_typet.

Definition at line 1462 of file std_types.h.

◆ to_floatbv_type() [2/2]

floatbv_typet& to_floatbv_type ( typet type)
inline

Cast a typet to a floatbv_typet.

This is an unchecked conversion. type must be known to be floatbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type floatbv_typet.

Definition at line 1471 of file std_types.h.

◆ to_incomplete_array_type() [1/2]

const incomplete_array_typet& to_incomplete_array_type ( const typet type)
inline

Cast a typet to an incomplete_array_typet.

This is an unchecked conversion. type must be known to be incomplete_array_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type incomplete_array_typet.

Definition at line 1108 of file std_types.h.

◆ to_incomplete_array_type() [2/2]

incomplete_array_typet& to_incomplete_array_type ( typet type)
inline

Cast a typet to an incomplete_array_typet.

This is an unchecked conversion. type must be known to be incomplete_array_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type incomplete_array_typet.

Definition at line 1115 of file std_types.h.

◆ to_pointer_type() [1/2]

const pointer_typet& to_pointer_type ( const typet type)
inline

Cast a typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type pointer_typet.

Definition at line 1564 of file std_types.h.

◆ to_pointer_type() [2/2]

pointer_typet& to_pointer_type ( typet type)
inline

Cast a typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type pointer_typet.

Definition at line 1573 of file std_types.h.

◆ to_range_type() [1/2]

const range_typet& to_range_type ( const typet type)
inline

Cast a typet to a range_typet.

This is an unchecked conversion. type must be known to be range_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type range_typet.

Definition at line 1754 of file std_types.h.

◆ to_range_type() [2/2]

range_typet& to_range_type ( typet type)
inline

Cast a typet to a range_typet.

This is an unchecked conversion. type must be known to be range_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type range_typet.

Definition at line 1761 of file std_types.h.

◆ to_reference_type() [1/2]

const reference_typet& to_reference_type ( const typet type)
inline

Cast a typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type reference_typet.

Definition at line 1613 of file std_types.h.

◆ to_reference_type() [2/2]

reference_typet& to_reference_type ( typet type)
inline

Cast a typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type reference_typet.

Definition at line 1620 of file std_types.h.

◆ to_signedbv_type() [1/2]

const signedbv_typet& to_signedbv_type ( const typet type)
inline

Cast a typet to a signedbv_typet.

This is an unchecked conversion. type must be known to be signedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type signedbv_typet.

Definition at line 1336 of file std_types.h.

◆ to_signedbv_type() [2/2]

signedbv_typet& to_signedbv_type ( typet type)
inline

Cast a typet to a signedbv_typet.

This is an unchecked conversion. type must be known to be signedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type signedbv_typet.

Definition at line 1345 of file std_types.h.

◆ to_string_type() [1/2]

const string_typet& to_string_type ( const typet type)
inline

Cast a typet to a string_typet.

This is an unchecked conversion. type must be known to be string_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type string_typet.

Definition at line 1707 of file std_types.h.

◆ to_string_type() [2/2]

string_typet& to_string_type ( typet type)
inline

Cast a typet to a string_typet.

This is an unchecked conversion. type must be known to be string_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type string_typet.

Definition at line 1714 of file std_types.h.

◆ to_struct_tag_type() [1/2]

const struct_tag_typet& to_struct_tag_type ( const typet type)
inline

Cast a typet to a struct_tag_typet.

This is an unchecked conversion. type must be known to be struct_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type struct_tag_typet

Definition at line 564 of file std_types.h.

◆ to_struct_tag_type() [2/2]

struct_tag_typet& to_struct_tag_type ( typet type)
inline

Cast a typet to a struct_tag_typet.

This is an unchecked conversion. type must be known to be struct_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type struct_tag_typet

Definition at line 571 of file std_types.h.

◆ to_struct_type() [1/2]

const struct_typet& to_struct_type ( const typet type)
inline

Cast a typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type struct_typet.

Definition at line 370 of file std_types.h.

◆ to_struct_type() [2/2]

struct_typet& to_struct_type ( typet type)
inline

Cast a typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type struct_typet.

Definition at line 377 of file std_types.h.

◆ to_struct_union_type() [1/2]

const struct_union_typet& to_struct_union_type ( const typet type)
inline

Cast a typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type
Returns
Object of type struct_union_typet

Definition at line 262 of file std_types.h.

◆ to_struct_union_type() [2/2]

struct_union_typet& to_struct_union_type ( typet type)
inline

Cast a typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type
Returns
Object of type struct_union_typet

Definition at line 269 of file std_types.h.

◆ to_symbol_type() [1/2]

const symbol_typet& to_symbol_type ( const typet type)
inline

Cast a typet to a symbol_typet.

This is an unchecked conversion. type must be known to be symbol_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type symbol_typet.

Definition at line 98 of file std_types.h.

◆ to_symbol_type() [2/2]

symbol_typet& to_symbol_type ( typet type)
inline

Cast a typet to a symbol_typet.

This is an unchecked conversion. type must be known to be symbol_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type symbol_typet.

Definition at line 105 of file std_types.h.

◆ to_tag_type() [1/2]

const tag_typet& to_tag_type ( const typet type)
inline

Cast a typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type tag_typet.

Definition at line 524 of file std_types.h.

◆ to_tag_type() [2/2]

tag_typet& to_tag_type ( typet type)
inline

Cast a typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type tag_typet.

Definition at line 531 of file std_types.h.

◆ to_union_tag_type() [1/2]

const union_tag_typet& to_union_tag_type ( const typet type)
inline

Cast a typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type union_tag_typet.

Definition at line 604 of file std_types.h.

◆ to_union_tag_type() [2/2]

union_tag_typet& to_union_tag_type ( typet type)
inline

Cast a typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type union_tag_typet.

Definition at line 611 of file std_types.h.

◆ to_union_type() [1/2]

const union_typet& to_union_type ( const typet type)
inline

Cast a typet to a union_typet.

This is an unchecked conversion. type must be known to be union_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type union_typet

Definition at line 471 of file std_types.h.

◆ to_union_type() [2/2]

union_typet& to_union_type ( typet type)
inline

Cast a typet to a union_typet.

This is an unchecked conversion. type must be known to be union_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type union_typet

Definition at line 478 of file std_types.h.

◆ to_unsignedbv_type() [1/2]

const unsignedbv_typet& to_unsignedbv_type ( const typet type)
inline

Cast a typet to an unsignedbv_typet.

This is an unchecked conversion. type must be known to be unsignedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type unsignedbv_typet.

Definition at line 1282 of file std_types.h.

◆ to_unsignedbv_type() [2/2]

unsignedbv_typet& to_unsignedbv_type ( typet type)
inline

Cast a typet to an unsignedbv_typet.

This is an unchecked conversion. type must be known to be unsignedbv_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type unsignedbv_typet.

Definition at line 1290 of file std_types.h.

◆ to_vector_type() [1/2]

const vector_typet& to_vector_type ( const typet type)
inline

Cast a typet to a vector_typet.

This is an unchecked conversion. type must be known to be vector_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type vector_typet.

Definition at line 1813 of file std_types.h.

◆ to_vector_type() [2/2]

vector_typet& to_vector_type ( typet type)
inline

Cast a typet to a vector_typet.

This is an unchecked conversion. type must be known to be vector_typet. Will fail with a precondition violation if type doesn't match.

Parameters
typeSource type.
Returns
Object of type vector_typet.

Definition at line 1820 of file std_types.h.

◆ validate_type() [1/6]

void validate_type ( const bv_typet type)
inline

Definition at line 1212 of file std_types.h.

◆ validate_type() [2/6]

void validate_type ( const signedbv_typet type)
inline

Definition at line 1322 of file std_types.h.

◆ validate_type() [3/6]

void validate_type ( const fixedbv_typet type)
inline

Definition at line 1386 of file std_types.h.

◆ validate_type() [4/6]

void validate_type ( const floatbv_typet type)
inline

Definition at line 1448 of file std_types.h.

◆ validate_type() [5/6]

void validate_type ( const pointer_typet type)
inline

Definition at line 1551 of file std_types.h.

◆ validate_type() [6/6]

void validate_type ( const c_bool_typet type)
inline

Definition at line 1649 of file std_types.h.