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 69 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 292 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 354 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 128 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 228 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 178 of file bitvector_types.h.
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 82 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 90 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 305 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 313 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 367 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 375 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 142 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 150 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 241 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 249 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 191 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 199 of file bitvector_types.h.