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... | |
void | validate_type (const reference_typet &type) |
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 998 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 1064 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 1126 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 1458 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 1623 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 708 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 668 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 933 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 1802 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 592 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 1349 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 1411 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 1185 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 1513 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 1713 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 1566 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 1285 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 1666 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 502 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 461 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 542 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 409 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 1235 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 1762 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 200 of file std_types.cpp.
bool is_reference | ( | const typet & | type | ) |
Returns true if the type is a reference.
Definition at line 133 of file std_types.cpp.
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.
|
inline |
This method tests, if the given typet is a signed or unsigned bitvector.
Definition at line 1076 of file std_types.h.
|
inline |
This method tests, if the given typet is a pointer of type void.
Definition at line 1543 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 1011 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 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 1089 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 1097 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 1139 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 1147 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 1471 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_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 1636 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 1644 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 721 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 728 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 681 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 688 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 946 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 954 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 1815 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 1822 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 605 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 612 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 1362 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 1370 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 1424 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 1432 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 1199 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 1207 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 1526 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 1534 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 1726 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 1733 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 1585 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 1592 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 1298 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 1306 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 1679 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 1686 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 515 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 522 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 475 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 482 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 555 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 562 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 422 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 429 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 1248 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 1256 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 1775 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 1782 of file std_types.h.
|
inline |
Definition at line 1571 of file std_types.h.