cprover
|
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>
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_typet & | to_struct_union_type (const typet &type) |
Cast a typet to a struct_union_typet. More... | |
struct_union_typet & | to_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_typet & | to_struct_type (const typet &type) |
Cast a typet to a struct_typet. More... | |
struct_typet & | to_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_typet & | to_class_type (const typet &type) |
Cast a typet to a class_typet. More... | |
class_typet & | to_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_typet & | to_union_type (const typet &type) |
Cast a typet to a union_typet. More... | |
union_typet & | to_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_typet & | to_tag_type (const typet &type) |
Cast a typet to a tag_typet. More... | |
tag_typet & | to_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_typet & | to_struct_tag_type (const typet &type) |
Cast a typet to a struct_tag_typet. More... | |
struct_tag_typet & | to_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_typet & | to_union_tag_type (const typet &type) |
Cast a typet to a union_tag_typet. More... | |
union_tag_typet & | to_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_typet & | to_enumeration_type (const typet &type) |
Cast a typet to a enumeration_typet. More... | |
enumeration_typet & | to_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_typet & | to_c_enum_type (const typet &type) |
Cast a typet to a c_enum_typet. More... | |
c_enum_typet & | to_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_typet & | to_c_enum_tag_type (const typet &type) |
Cast a typet to a c_enum_tag_typet. More... | |
c_enum_tag_typet & | to_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_typet & | to_code_type (const typet &type) |
Cast a typet to a code_typet. More... | |
code_typet & | to_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_typet & | to_array_type (const typet &type) |
Cast a typet to an array_typet. More... | |
array_typet & | to_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_typet & | to_bitvector_type (const typet &type) |
Cast a typet to a bitvector_typet. More... | |
bitvector_typet & | to_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_typet & | to_bv_type (const typet &type) |
Cast a typet to a bv_typet. More... | |
bv_typet & | to_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_typet & | to_integer_bitvector_type (const typet &type) |
Cast a typet to an integer_bitvector_typet. More... | |
integer_bitvector_typet & | to_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_typet & | to_unsignedbv_type (const typet &type) |
Cast a typet to an unsignedbv_typet. More... | |
unsignedbv_typet & | to_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_typet & | to_signedbv_type (const typet &type) |
Cast a typet to a signedbv_typet. More... | |
signedbv_typet & | to_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_typet & | to_fixedbv_type (const typet &type) |
Cast a typet to a fixedbv_typet. More... | |
fixedbv_typet & | to_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_typet & | to_floatbv_type (const typet &type) |
Cast a typet to a floatbv_typet. More... | |
floatbv_typet & | to_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_typet & | to_c_bit_field_type (const typet &type) |
Cast a typet to a c_bit_field_typet. More... | |
c_bit_field_typet & | to_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_typet & | to_pointer_type (const typet &type) |
Cast a typet to a pointer_typet. More... | |
pointer_typet & | to_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_typet & | to_reference_type (const typet &type) |
Cast a typet to a reference_typet. More... | |
reference_typet & | to_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_typet & | to_c_bool_type (const typet &type) |
Cast a typet to a c_bool_typet. More... | |
c_bool_typet & | to_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_typet & | to_string_type (const typet &type) |
Cast a typet to a string_typet. More... | |
string_typet & | to_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_typet & | to_range_type (const typet &type) |
Cast a typet to a range_typet. More... | |
range_typet & | to_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_typet & | to_vector_type (const typet &type) |
Cast a typet to a vector_typet. More... | |
vector_typet & | to_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_typet & | to_complex_type (const typet &type) |
Cast a typet to a complex_typet. More... | |
complex_typet & | to_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... | |
Pre-defined types.
Definition in file std_types.h.
|
inline |
Check whether a reference to a typet is a array_typet.
type | Source type. |
type
is a array_typet. Definition at line 1005 of file std_types.h.
|
inline |
Check whether a reference to a typet is a bitvector_typet.
type | Source type. |
type
is a bitvector_typet. Definition at line 1071 of file std_types.h.
|
inline |
Check whether a reference to a typet is a bv_typet.
type | Source type. |
type
is a bv_typet. Definition at line 1133 of file std_types.h.
|
inline |
Check whether a reference to a typet is a c_bit_field_typet.
type | Source type. |
type
is a c_bit_field_typet. Definition at line 1465 of file std_types.h.
|
inline |
Check whether a reference to a typet is a c_bool_typet.
type | Source type. |
type
is a c_bool_typet. Definition at line 1637 of file std_types.h.
|
inline |
Check whether a reference to a typet is a c_enum_tag_typet.
type | Source type. |
type
is a c_enum_tag_typet. Definition at line 716 of file std_types.h.
|
inline |
Check whether a reference to a typet is a c_enum_typet.
type | Source type. |
type
is a c_enum_typet. Definition at line 676 of file std_types.h.
|
inline |
Check whether a reference to a typet is a class_typet.
type | Source type. |
type
is a class_typet. Definition at line 363 of file std_types.h.
|
inline |
Check whether a reference to a typet is a code_typet.
type | Source type. |
type
is a code_typet. Definition at line 936 of file std_types.h.
|
inline |
Check whether a reference to a typet is a complex_typet.
type | Source type. |
type
is a complex_typet. Definition at line 1816 of file std_types.h.
|
inline |
Check whether a reference to a typet is a enumeration_typet.
type | Source type. |
type
is a enumeration_typet. Definition at line 600 of file std_types.h.
|
inline |
Check whether a reference to a typet is a fixedbv_typet.
type | Source type. |
type
is a fixedbv_typet. Definition at line 1356 of file std_types.h.
|
inline |
Check whether a reference to a typet is a floatbv_typet.
type | Source type. |
type
is a floatbv_typet. Definition at line 1418 of file std_types.h.
|
inline |
Check whether a reference to a typet is an integer_bitvector_typet.
type | Source type. |
type
is an integer_bitvector_typet. Definition at line 1192 of file std_types.h.
|
inline |
Check whether a reference to a typet is a pointer_typet.
type | Source type. |
type
is a pointer_typet. Definition at line 1520 of file std_types.h.
|
inline |
Check whether a reference to a typet is a range_typet.
type | Source type. |
type
is a range_typet. Definition at line 1727 of file std_types.h.
|
inline |
Check whether a reference to a typet is a reference_typet.
type | Source type. |
type
is a reference_typet. Definition at line 1586 of file std_types.h.
|
inline |
Check whether a reference to a typet is a signedbv_typet.
type | Source type. |
type
is a signedbv_typet. Definition at line 1292 of file std_types.h.
|
inline |
Check whether a reference to a typet is a string_typet.
type | Source type. |
type
is a string_typet. Definition at line 1680 of file std_types.h.
|
inline |
Check whether a reference to a typet is a struct_tag_typet.
type | Source type. |
type
is a struct_tag_typet. Definition at line 510 of file std_types.h.
|
inline |
Check whether a reference to a typet is a struct_typet.
type | Source type. |
type
is a struct_typet. Definition at line 290 of file std_types.h.
|
inline |
Check whether a reference to a typet is a struct_union_typet.
type | Source type. |
type
is a struct_union_typet. Definition at line 196 of file std_types.h.
|
inline |
Check whether a reference to a typet is a tag_typet.
type | Source type. |
type
is a tag_typet. Definition at line 469 of file std_types.h.
|
inline |
Check whether a reference to a typet is a union_tag_typet.
type | Source type. |
type
is a union_tag_typet. Definition at line 550 of file std_types.h.
|
inline |
Check whether a reference to a typet is a union_typet.
type | Source type. |
type
is a union_typet. Definition at line 417 of file std_types.h.
|
inline |
Check whether a reference to a typet is a unsignedbv_typet.
type | Source type. |
type
is a unsignedbv_typet. Definition at line 1242 of file std_types.h.
|
inline |
Check whether a reference to a typet is a vector_typet.
type | Source type. |
type
is a vector_typet. Definition at line 1776 of file std_types.h.
|
inline |
This method tests, if the given typet is a constant.
Definition at line 30 of file std_types.h.
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:
type | The type we want to query constness of. |
ns | The namespace, needed for resolution of symbols. |
Definition at line 214 of file std_types.cpp.
bool is_reference | ( | const typet & | type | ) |
Returns true if the type is a reference.
Definition at line 147 of file std_types.cpp.
bool is_rvalue_reference | ( | const typet & | type | ) |
Returns if the type is an R value reference.
Definition at line 154 of file std_types.cpp.
|
inline |
This method tests, if the given typet is a signed or unsigned bitvector.
Definition at line 1083 of file std_types.h.
|
inline |
This method tests, if the given typet is a pointer of type void.
Definition at line 1550 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1018 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1025 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1096 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1104 of file std_types.h.
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.
type | Source type. |
Definition at line 1146 of file std_types.h.
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.
type | Source type. |
Definition at line 1154 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1478 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1485 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1650 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1658 of file std_types.h.
|
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.
type | Source type. |
Definition at line 729 of file std_types.h.
|
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.
type | Source type. |
Definition at line 736 of file std_types.h.
|
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.
type | Source type. |
Definition at line 689 of file std_types.h.
|
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.
type | Source type. |
Definition at line 696 of file std_types.h.
|
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.
type | Source type. |
Definition at line 376 of file std_types.h.
|
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.
type | Source type. |
Definition at line 383 of file std_types.h.
|
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.
type | Source type. |
Definition at line 949 of file std_types.h.
|
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.
type | Source type. |
Definition at line 957 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1829 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1836 of file std_types.h.
|
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.
type | Source type. |
Definition at line 613 of file std_types.h.
|
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.
type | Source type. |
Definition at line 620 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1369 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1377 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1431 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1439 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1206 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1214 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1533 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1541 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1740 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1747 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1599 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1606 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1305 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1313 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1693 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1700 of file std_types.h.
|
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.
type | Source type. |
Definition at line 523 of file std_types.h.
|
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.
type | Source type. |
Definition at line 530 of file std_types.h.
|
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.
type | Source type. |
Definition at line 303 of file std_types.h.
|
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.
type | Source type. |
Definition at line 310 of file std_types.h.
|
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.
type | Source type |
Definition at line 209 of file std_types.h.
|
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.
type | Source type |
Definition at line 216 of file std_types.h.
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.
type | Source type. |
Definition at line 483 of file std_types.h.
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.
type | Source type. |
Definition at line 490 of file std_types.h.
|
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.
type | Source type. |
Definition at line 563 of file std_types.h.
|
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.
type | Source type. |
Definition at line 570 of file std_types.h.
|
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.
type | Source type. |
Definition at line 430 of file std_types.h.
|
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.
type | Source type. |
Definition at line 437 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1255 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1263 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1789 of file std_types.h.
|
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.
type | Source type. |
Definition at line 1796 of file std_types.h.