Pre-defined bitvector types. More...

#include "expr_cast.h"
#include "mp_arith.h"
#include "type.h"

Include dependency graph for bitvector_types.h:

This graph shows which files directly or indirectly include this file:

Classes
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...

Functions
template<>
bool	can_cast_type< bitvector_typet > (const typet &type)
	Check whether a reference to a typet is a bitvector_typet.

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.

Detailed Description

Pre-defined bitvector types.

Definition in file bitvector_types.h.

Function Documentation

◆ can_cast_type< bitvector_typet >()

template<>

bool can_cast_type< bitvector_typet > ( const typet & type )

inline

Check whether a reference to a typet is a bitvector_typet.

Parameters

type	Source type.

Returns: True if type is a bitvector_typet.

Definition at line 74 of file bitvector_types.h.

◆ can_cast_type< bv_typet >()

template<>

bool can_cast_type< bv_typet > ( const typet & type )

inline

Check whether a reference to a typet is a bv_typet.

Parameters

type	Source type.

Returns: True if type is a bv_typet.

Definition at line 136 of file bitvector_types.h.

◆ can_cast_type< fixedbv_typet >()

template<>

bool can_cast_type< fixedbv_typet > ( const typet & type )

inline

Check whether a reference to a typet is a fixedbv_typet.

Parameters

type	Source type.

Returns: True if type is a fixedbv_typet.

Definition at line 374 of file bitvector_types.h.

◆ can_cast_type< floatbv_typet >()

template<>

bool can_cast_type< floatbv_typet > ( const typet & type )

inline

Check whether a reference to a typet is a floatbv_typet.

Parameters

type	Source type.

Returns: True if type is a floatbv_typet.

Definition at line 436 of file bitvector_types.h.

◆ can_cast_type< integer_bitvector_typet >()

template<>

bool can_cast_type< integer_bitvector_typet > ( const typet & type )

inline

Check whether a reference to a typet is an integer_bitvector_typet.

Parameters

type	Source type.

Returns: True if type is an integer_bitvector_typet.

Definition at line 200 of file bitvector_types.h.

◆ can_cast_type< signedbv_typet >()

template<>

bool can_cast_type< signedbv_typet > ( const typet & type )

inline

Check whether a reference to a typet is a signedbv_typet.

Parameters

type	Source type.

Returns: True if type is a signedbv_typet.

Definition at line 310 of file bitvector_types.h.

◆ can_cast_type< unsignedbv_typet >()

template<>

bool can_cast_type< unsignedbv_typet > ( const typet & type )

inline

Check whether a reference to a typet is a unsignedbv_typet.

Parameters

type	Source type.

Returns: True if type is a unsignedbv_typet.

Definition at line 255 of file bitvector_types.h.

◆ is_signed_or_unsigned_bitvector()

bool is_signed_or_unsigned_bitvector ( const typet & type )

inline

This method tests, if the given typet is a signed or unsigned bitvector.

Definition at line 86 of file bitvector_types.h.

◆ to_bitvector_type() [1/2]

const bitvector_typet & to_bitvector_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type bitvector_typet.

Definition at line 99 of file bitvector_types.h.

◆ to_bitvector_type() [2/2]

bitvector_typet & to_bitvector_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type bitvector_typet.

Definition at line 107 of file bitvector_types.h.

◆ to_bv_type() [1/2]

const bv_typet & to_bv_type ( const typet & type )

inline

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.

Parameters

type	Source type.

Returns: Object of type bv_typet.

Definition at line 149 of file bitvector_types.h.

◆ to_bv_type() [2/2]

bv_typet & to_bv_type ( typet & type )

inline

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.

Parameters

type	Source type.

Returns: Object of type bv_typet.

Definition at line 157 of file bitvector_types.h.

◆ to_fixedbv_type() [1/2]

const fixedbv_typet & to_fixedbv_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type fixedbv_typet.

Definition at line 387 of file bitvector_types.h.

◆ to_fixedbv_type() [2/2]

fixedbv_typet & to_fixedbv_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type fixedbv_typet.

Definition at line 395 of file bitvector_types.h.

◆ to_floatbv_type() [1/2]

const floatbv_typet & to_floatbv_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type floatbv_typet.

Definition at line 449 of file bitvector_types.h.

◆ to_floatbv_type() [2/2]

floatbv_typet & to_floatbv_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type floatbv_typet.

Definition at line 457 of file bitvector_types.h.

◆ to_integer_bitvector_type() [1/2]

const integer_bitvector_typet & to_integer_bitvector_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type integer_bitvector_typet.

Definition at line 214 of file bitvector_types.h.

◆ to_integer_bitvector_type() [2/2]

integer_bitvector_typet & to_integer_bitvector_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type integer_bitvector_typet.

Definition at line 222 of file bitvector_types.h.

◆ to_signedbv_type() [1/2]

const signedbv_typet & to_signedbv_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type signedbv_typet.

Definition at line 323 of file bitvector_types.h.

◆ to_signedbv_type() [2/2]

signedbv_typet & to_signedbv_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type signedbv_typet.

Definition at line 331 of file bitvector_types.h.

◆ to_unsignedbv_type() [1/2]

const unsignedbv_typet & to_unsignedbv_type ( const typet & type )

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.

Parameters

type	Source type.

Returns: Object of type unsignedbv_typet.

Definition at line 268 of file bitvector_types.h.

◆ to_unsignedbv_type() [2/2]

unsignedbv_typet & to_unsignedbv_type ( typet & type )

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.

Parameters

type	Source type.

Returns: Object of type unsignedbv_typet.

Definition at line 276 of file bitvector_types.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_type< bitvector_typet >()

◆ can_cast_type< bv_typet >()

◆ can_cast_type< fixedbv_typet >()

◆ can_cast_type< floatbv_typet >()

◆ can_cast_type< integer_bitvector_typet >()

◆ can_cast_type< signedbv_typet >()

◆ can_cast_type< unsignedbv_typet >()

◆ is_signed_or_unsigned_bitvector()

◆ to_bitvector_type() [1/2]

◆ to_bitvector_type() [2/2]

◆ to_bv_type() [1/2]

◆ to_bv_type() [2/2]

◆ to_fixedbv_type() [1/2]

◆ to_fixedbv_type() [2/2]

◆ to_floatbv_type() [1/2]

◆ to_floatbv_type() [2/2]

◆ to_integer_bitvector_type() [1/2]

◆ to_integer_bitvector_type() [2/2]

◆ to_signedbv_type() [1/2]

◆ to_signedbv_type() [2/2]

◆ to_unsignedbv_type() [1/2]

◆ to_unsignedbv_type() [2/2]