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  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

bool is_constant (const typet &type)
 This method tests, if the given typet is a constant. 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< bitvector_typet > (const typet &type)
 Check whether a reference to a typet is a bitvector_typet. More...
 
bool is_signed_or_unsigned_bitvector (const typet &type)
 This method tests, if the given typet is a signed or unsigned bitvector. 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...
 
bool is_void_pointer (const typet &type)
 This method tests, if the given typet is a pointer of type void. 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 998 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 1064 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 1126 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 1458 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 1618 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 708 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 668 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 363 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 933 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 1802 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 592 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 1349 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 1411 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 1185 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 1513 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 1708 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 1566 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 1285 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 1661 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 502 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 290 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 196 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 461 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 542 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 409 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 1235 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 1757 of file std_types.h.

◆ is_constant()

bool is_constant ( const typet type)
inline

This method tests, if the given typet is a constant.

Definition at line 30 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.

◆ is_signed_or_unsigned_bitvector()

bool is_signed_or_unsigned_bitvector ( const typet type)
inline

This method tests, if the given typet is a signed or unsigned bitvector.

Definition at line 1076 of file std_types.h.

◆ is_void_pointer()

bool is_void_pointer ( const typet type)
inline

This method tests, if the given typet is a pointer of type void.

Definition at line 1543 of file std_types.h.

◆ 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 1011 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 1018 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 1089 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 1097 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 1139 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 1147 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 1471 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 1478 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 1631 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 1639 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 721 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 728 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 681 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 688 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 376 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 383 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 946 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 954 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 1815 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 1822 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 605 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 612 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 1362 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 1370 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 1424 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 1432 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 1199 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 1207 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 1526 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 1534 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 1721 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 1728 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 1580 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 1587 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 1298 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 1306 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 1674 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 1681 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 515 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 522 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 303 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 310 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 209 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 216 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 475 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 482 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 555 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 562 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 422 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 429 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 1248 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 1256 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 1770 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 1777 of file std_types.h.