cprover
|
Pre-defined types. More...
#include "expr.h"
#include "expr_cast.h"
#include "invariant.h"
#include "mp_arith.h"
#include "validate.h"
#include <unordered_map>
Go to the source code of this file.
Classes | |
class | bool_typet |
The Boolean type. More... | |
class | nil_typet |
The NIL type, i.e., an invalid type, no value. More... | |
class | empty_typet |
The empty type. More... | |
class | void_typet |
The void type, the same as empty_typet. More... | |
class | symbol_typet |
A reference into the symbol table. More... | |
class | struct_union_typet |
Base type for structs and unions. More... | |
class | struct_union_typet::componentt |
class | struct_typet |
Structure type, corresponds to C style structs. More... | |
class | struct_typet::baset |
Base class or struct that a class or struct inherits from. More... | |
class | class_typet |
Class type. More... | |
class | union_typet |
The union type. More... | |
class | tag_typet |
A tag-based type, i.e., typet with an identifier. More... | |
class | struct_tag_typet |
A struct tag type, i.e., struct_typet with an identifier. More... | |
class | union_tag_typet |
A union tag type, i.e., union_typet with an identifier. More... | |
class | enumeration_typet |
An enumeration type, i.e., a type with elements (not to be confused with C enums) More... | |
class | c_enum_typet |
The type of C enums. More... | |
class | c_enum_typet::c_enum_membert |
class | c_enum_tag_typet |
C enum tag type, i.e., c_enum_typet with an identifier. More... | |
class | code_typet |
Base type of functions. More... | |
class | code_typet::parametert |
class | array_typet |
Arrays with given size. More... | |
class | incomplete_array_typet |
Arrays without size. More... | |
class | bitvector_typet |
Base class of fixed-width bit-vector types. More... | |
class | bv_typet |
Fixed-width bit-vector without numerical interpretation. More... | |
class | unsignedbv_typet |
Fixed-width bit-vector with unsigned binary interpretation. More... | |
class | signedbv_typet |
Fixed-width bit-vector with two's complement interpretation. More... | |
class | fixedbv_typet |
Fixed-width bit-vector with signed fixed-point interpretation. More... | |
class | floatbv_typet |
Fixed-width bit-vector with IEEE floating-point interpretation. More... | |
class | c_bit_field_typet |
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More... | |
class | pointer_typet |
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More... | |
class | reference_typet |
The reference type. More... | |
class | c_bool_typet |
The C/C++ Booleans. More... | |
class | string_typet |
String type. More... | |
class | range_typet |
A type for subranges of integers. More... | |
class | vector_typet |
The vector type. More... | |
class | complex_typet |
Complex numbers made of pair of given subtype. More... | |
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 1035 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 1140 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 1187 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 1478 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 1624 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 724 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 684 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 396 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 969 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 1825 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 620 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 1361 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 1423 of file std_types.h.
|
inline |
Check whether a reference to a typet is a incomplete_array_typet.
type | Source type. |
type
is a incomplete_array_typet. Definition at line 1074 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 1526 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 1721 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 1579 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 1297 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 1674 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 530 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 336 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 247 of file std_types.h.
|
inline |
Check whether a reference to a typet is a symbol_typet.
type | Source type. |
type
is a symbol_typet. Definition at line 85 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 489 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 570 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 437 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 1249 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 1780 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 224 of file std_types.cpp.
bool is_reference | ( | const typet & | type | ) |
Returns true if the type is a reference.
Definition at line 132 of file std_types.cpp.
bool is_rvalue_reference | ( | const typet & | type | ) |
Returns if the type is an R value reference.
Definition at line 139 of file std_types.cpp.
|
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 1048 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 1055 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 1158 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 1166 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 1205 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 1214 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 1491 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 1498 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 1642 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 1651 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 737 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 744 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 697 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 704 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 409 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 416 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 982 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 990 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 1838 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 1845 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 633 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 640 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 1380 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 1389 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 1442 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 1451 of file std_types.h.
|
inline |
Cast a typet to an incomplete_array_typet.
This is an unchecked conversion. type must be known to be incomplete_array_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 1087 of file std_types.h.
|
inline |
Cast a typet to an incomplete_array_typet.
This is an unchecked conversion. type must be known to be incomplete_array_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 1094 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 1544 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 1553 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 1734 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 1741 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 1593 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 1600 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 1316 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 1325 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 1687 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 1694 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 543 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 550 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 349 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 356 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 260 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 267 of file std_types.h.
|
inline |
Cast a typet to a symbol_typet.
This is an unchecked conversion. type must be known to be symbol_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 98 of file std_types.h.
|
inline |
Cast a typet to a symbol_typet.
This is an unchecked conversion. type must be known to be symbol_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 105 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 503 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 510 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 583 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 590 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 450 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 457 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 1262 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 1270 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 1793 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 1800 of file std_types.h.
|
inline |
Definition at line 1192 of file std_types.h.
|
inline |
Definition at line 1302 of file std_types.h.
|
inline |
Definition at line 1366 of file std_types.h.
|
inline |
Definition at line 1428 of file std_types.h.
|
inline |
Definition at line 1531 of file std_types.h.
|
inline |
Definition at line 1629 of file std_types.h.