Pre-defined bitvector types. More...

#include "std_types.h"

Include dependency graph for bitvector_types.h:

This graph shows which files directly or indirectly include 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. 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...

Detailed Description

Pre-defined bitvector types.

Definition in file bitvector_types.h.

Function Documentation

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

Classes

Functions

Detailed Description

Function Documentation

◆ 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]