cprover
|
Pre-defined bitvector types. More...
#include "std_types.h"
Go to the source code of this file.
Classes | |
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... |
Functions | |
bool | is_signed_or_unsigned_bitvector (const typet &type) |
This method tests, if the given typet is a signed or unsigned bitvector. | |
const bitvector_typet & | to_bitvector_type (const typet &type) |
Cast a typet to a bitvector_typet. | |
bitvector_typet & | to_bitvector_type (typet &type) |
Cast a typet to a bitvector_typet. | |
template<> | |
bool | can_cast_type< bv_typet > (const typet &type) |
Check whether a reference to a typet is a bv_typet. | |
const bv_typet & | to_bv_type (const typet &type) |
Cast a typet to a bv_typet. | |
bv_typet & | to_bv_type (typet &type) |
Cast a typet to a bv_typet. | |
template<> | |
bool | can_cast_type< integer_bitvector_typet > (const typet &type) |
Check whether a reference to a typet is an integer_bitvector_typet. | |
const integer_bitvector_typet & | to_integer_bitvector_type (const typet &type) |
Cast a typet to an integer_bitvector_typet. | |
integer_bitvector_typet & | to_integer_bitvector_type (typet &type) |
Cast a typet to an integer_bitvector_typet. | |
template<> | |
bool | can_cast_type< unsignedbv_typet > (const typet &type) |
Check whether a reference to a typet is a unsignedbv_typet. | |
const unsignedbv_typet & | to_unsignedbv_type (const typet &type) |
Cast a typet to an unsignedbv_typet. | |
unsignedbv_typet & | to_unsignedbv_type (typet &type) |
Cast a typet to an unsignedbv_typet. | |
template<> | |
bool | can_cast_type< signedbv_typet > (const typet &type) |
Check whether a reference to a typet is a signedbv_typet. | |
const signedbv_typet & | to_signedbv_type (const typet &type) |
Cast a typet to a signedbv_typet. | |
signedbv_typet & | to_signedbv_type (typet &type) |
Cast a typet to a signedbv_typet. | |
template<> | |
bool | can_cast_type< fixedbv_typet > (const typet &type) |
Check whether a reference to a typet is a fixedbv_typet. | |
const fixedbv_typet & | to_fixedbv_type (const typet &type) |
Cast a typet to a fixedbv_typet. | |
fixedbv_typet & | to_fixedbv_type (typet &type) |
Cast a typet to a fixedbv_typet. | |
template<> | |
bool | can_cast_type< floatbv_typet > (const typet &type) |
Check whether a reference to a typet is a floatbv_typet. | |
const floatbv_typet & | to_floatbv_type (const typet &type) |
Cast a typet to a floatbv_typet. | |
floatbv_typet & | to_floatbv_type (typet &type) |
Cast a typet to a floatbv_typet. |
Pre-defined bitvector types.
Definition in file bitvector_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 73 of file bitvector_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 311 of file bitvector_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 373 of file bitvector_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 137 of file bitvector_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 247 of file bitvector_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 192 of file bitvector_types.h.
|
inline |
This method tests, if the given typet is a signed or unsigned bitvector.
Definition at line 19 of file bitvector_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 32 of file bitvector_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 40 of file bitvector_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 86 of file bitvector_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 94 of file bitvector_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 324 of file bitvector_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 332 of file bitvector_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 386 of file bitvector_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 394 of file bitvector_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 151 of file bitvector_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 159 of file bitvector_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 260 of file bitvector_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 268 of file bitvector_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 205 of file bitvector_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 213 of file bitvector_types.h.