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 <util/narrow.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  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  bitvector_typet
 Base class of fixed-width bit-vector types. More...
 
class  bv_typet
 Fixed-width bit-vector without numerical interpretation. More...
 
class  integer_bitvector_typet
 Fixed-width bit-vector representing a signed or unsigned integer. 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< 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< 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...
 
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< integer_bitvector_typet > (const typet &type)
 Check whether a reference to a typet is an integer_bitvector_typet. More...
 
const integer_bitvector_typetto_integer_bitvector_type (const typet &type)
 Cast a typet to an integer_bitvector_typet. More...
 
integer_bitvector_typetto_integer_bitvector_type (typet &type)
 Cast a typet to an integer_bitvector_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...
 
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...
 
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...
 
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...
 
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...
 
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 1010 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 1076 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 1131 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 1463 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 1616 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 710 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 670 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 365 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 945 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 1800 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 594 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 1354 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 1416 of file std_types.h.

◆ can_cast_type< integer_bitvector_typet >()

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

Check whether a reference to a typet is an integer_bitvector_typet.

Parameters
typeSource type.
Returns
True if type is an integer_bitvector_typet.

Definition at line 1190 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 1518 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 1706 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 1564 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 1290 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 1659 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 504 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 305 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 211 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 463 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 544 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 411 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 1240 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 1755 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 200 of file std_types.cpp.

◆ is_reference()

bool is_reference ( const typet type)

Returns true if the type is a reference.

Definition at line 133 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 140 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 1023 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 1030 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 1094 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 1102 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 1144 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 1152 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 1476 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 1483 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 1629 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 1637 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 723 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 730 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 683 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 690 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 378 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 385 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 958 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 966 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 1813 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 1820 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 607 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 614 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 1367 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 1375 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 1429 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 1437 of file std_types.h.

◆ to_integer_bitvector_type() [1/2]

const integer_bitvector_typet& to_integer_bitvector_type ( const typet type)
inline

Cast a typet to an integer_bitvector_typet.

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

Parameters
typeSource type.
Returns
Object of type integer_bitvector_typet.

Definition at line 1204 of file std_types.h.

◆ to_integer_bitvector_type() [2/2]

integer_bitvector_typet& to_integer_bitvector_type ( typet type)
inline

Cast a typet to an integer_bitvector_typet.

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

Parameters
typeSource type.
Returns
Object of type integer_bitvector_typet.

Definition at line 1212 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 1531 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 1539 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 1719 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 1726 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 1578 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 1585 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 1303 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 1311 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 1672 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 1679 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 517 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 524 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 318 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 325 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 224 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 231 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 477 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 484 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 557 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 564 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 424 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 431 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 1253 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 1261 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 1768 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 1775 of file std_types.h.