API to expression classes for bitvectors. More...

#include "std_expr.h"

Include dependency graph for bitvector_expr.h:

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

Classes
class	bswap_exprt
	The byte swap expression. More...

class	bitnot_exprt
	Bit-wise negation of bit-vectors. More...

class	bitor_exprt
	Bit-wise OR. More...

class	bitxor_exprt
	Bit-wise XOR. More...

class	bitxnor_exprt
	Bit-wise XNOR. More...

class	bitand_exprt
	Bit-wise AND. More...

class	shift_exprt
	A base class for shift and rotate operators. More...

class	shl_exprt
	Left shift. More...

class	ashr_exprt
	Arithmetic right shift. More...

class	lshr_exprt
	Logical right shift. More...

class	extractbit_exprt
	Extracts a single bit of a bit-vector operand. More...

class	extractbits_exprt
	Extracts a sub-range of a bit-vector operand. More...

class	update_bit_exprt
	Replaces a sub-range of a bit-vector operand. More...

class	update_bits_exprt
	Replaces a sub-range of a bit-vector operand. More...

class	replication_exprt
	Bit-vector replication. More...

class	concatenation_exprt
	Concatenation of bit-vector operands. More...

class	popcount_exprt
	The popcount (counting the number of bits set to 1) expression. More...

class	binary_overflow_exprt
	A Boolean expression returning true, iff operation `kind` would result in an overflow when applied to operands `lhs` and `rhs`. More...

class	plus_overflow_exprt

class	minus_overflow_exprt

class	mult_overflow_exprt

class	shl_overflow_exprt

class	unary_overflow_exprt
	A Boolean expression returning true, iff operation `kind` would result in an overflow when applied to the (single) operand. More...

class	unary_minus_overflow_exprt
	A Boolean expression returning true, iff negation would result in an overflow when applied to the (single) operand. More...

class	count_leading_zeros_exprt
	The count leading zeros (counting the number of zero bits starting from the most-significant bit) expression. More...

class	count_trailing_zeros_exprt
	The count trailing zeros (counting the number of zero bits starting from the least-significant bit) expression. More...

class	bitreverse_exprt
	Reverse the order of bits in a bit-vector. More...

class	saturating_plus_exprt
	The saturating plus expression. More...

class	saturating_minus_exprt
	Saturating subtraction expression. More...

class	overflow_result_exprt
	An expression returning both the result of the arithmetic operation under wrap-around semantics as well as a Boolean to signify overflow. More...

class	find_first_set_exprt
	Returns one plus the index of the least-significant one bit, or zero if the operand is zero. More...

class	zero_extend_exprt
	zero extension The operand is converted to the given type by either a) truncating if the new type is shorter, or b) padding with most-significant zero bits if the new type is larger, or c) reinterprets the operand as the given type if their widths match. More...

class	onehot_exprt
	A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwise. More...

class	onehot0_exprt
	A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwise. More...

Functions
template<>
bool	can_cast_expr< bswap_exprt > (const exprt &base)

void	validate_expr (const bswap_exprt &value)

const bswap_exprt &	to_bswap_expr (const exprt &expr)
	Cast an exprt to a bswap_exprt. More...

bswap_exprt &	to_bswap_expr (exprt &expr)
	Cast an exprt to a bswap_exprt. More...

template<>
bool	can_cast_expr< bitnot_exprt > (const exprt &base)

void	validate_expr (const bitnot_exprt &value)

const bitnot_exprt &	to_bitnot_expr (const exprt &expr)
	Cast an exprt to a bitnot_exprt. More...

bitnot_exprt &	to_bitnot_expr (exprt &expr)
	Cast an exprt to a bitnot_exprt. More...

template<>
bool	can_cast_expr< bitor_exprt > (const exprt &base)

const bitor_exprt &	to_bitor_expr (const exprt &expr)
	Cast an exprt to a bitor_exprt. More...

bitor_exprt &	to_bitor_expr (exprt &expr)
	Cast an exprt to a bitor_exprt. More...

template<>
bool	can_cast_expr< bitxor_exprt > (const exprt &base)

const bitxor_exprt &	to_bitxor_expr (const exprt &expr)
	Cast an exprt to a bitxor_exprt. More...

bitxor_exprt &	to_bitxor_expr (exprt &expr)
	Cast an exprt to a bitxor_exprt. More...

template<>
bool	can_cast_expr< bitxnor_exprt > (const exprt &base)

const bitxnor_exprt &	to_bitxnor_expr (const exprt &expr)
	Cast an exprt to a bitxnor_exprt. More...

bitxnor_exprt &	to_bitxnor_expr (exprt &expr)
	Cast an exprt to a bitxnor_exprt. More...

template<>
bool	can_cast_expr< bitand_exprt > (const exprt &base)

const bitand_exprt &	to_bitand_expr (const exprt &expr)
	Cast an exprt to a bitand_exprt. More...

bitand_exprt &	to_bitand_expr (exprt &expr)
	Cast an exprt to a bitand_exprt. More...

template<>
bool	can_cast_expr< shift_exprt > (const exprt &base)

void	validate_expr (const shift_exprt &value)

const shift_exprt &	to_shift_expr (const exprt &expr)
	Cast an exprt to a shift_exprt. More...

shift_exprt &	to_shift_expr (exprt &expr)
	Cast an exprt to a shift_exprt. More...

template<>
bool	can_cast_expr< shl_exprt > (const exprt &base)

const shl_exprt &	to_shl_expr (const exprt &expr)
	Cast an exprt to a shl_exprt. More...

shl_exprt &	to_shl_expr (exprt &expr)
	Cast an exprt to a shl_exprt. More...

template<>
bool	can_cast_expr< ashr_exprt > (const exprt &base)

template<>
bool	can_cast_expr< lshr_exprt > (const exprt &base)

template<>
bool	can_cast_expr< extractbit_exprt > (const exprt &base)

void	validate_expr (const extractbit_exprt &value)

const extractbit_exprt &	to_extractbit_expr (const exprt &expr)
	Cast an exprt to an extractbit_exprt. More...

extractbit_exprt &	to_extractbit_expr (exprt &expr)
	Cast an exprt to an extractbit_exprt. More...

template<>
bool	can_cast_expr< extractbits_exprt > (const exprt &base)

void	validate_expr (const extractbits_exprt &value)

const extractbits_exprt &	to_extractbits_expr (const exprt &expr)
	Cast an exprt to an extractbits_exprt. More...

extractbits_exprt &	to_extractbits_expr (exprt &expr)
	Cast an exprt to an extractbits_exprt. More...

template<>
bool	can_cast_expr< update_bit_exprt > (const exprt &base)

const update_bit_exprt &	to_update_bit_expr (const exprt &expr)
	Cast an exprt to an update_bit_exprt. More...

update_bit_exprt &	to_update_bit_expr (exprt &expr)
	Cast an exprt to an update_bit_exprt. More...

template<>
bool	can_cast_expr< update_bits_exprt > (const exprt &base)

const update_bits_exprt &	to_update_bits_expr (const exprt &expr)
	Cast an exprt to an update_bits_exprt. More...

update_bits_exprt &	to_update_bits_expr (exprt &expr)
	Cast an exprt to an update_bits_exprt. More...

template<>
bool	can_cast_expr< replication_exprt > (const exprt &base)

void	validate_expr (const replication_exprt &value)

const replication_exprt &	to_replication_expr (const exprt &expr)
	Cast an exprt to a replication_exprt. More...

replication_exprt &	to_replication_expr (exprt &expr)
	Cast an exprt to a replication_exprt. More...

template<>
bool	can_cast_expr< concatenation_exprt > (const exprt &base)

const concatenation_exprt &	to_concatenation_expr (const exprt &expr)
	Cast an exprt to a concatenation_exprt. More...

concatenation_exprt &	to_concatenation_expr (exprt &expr)
	Cast an exprt to a concatenation_exprt. More...

template<>
bool	can_cast_expr< popcount_exprt > (const exprt &base)

void	validate_expr (const popcount_exprt &value)

const popcount_exprt &	to_popcount_expr (const exprt &expr)
	Cast an exprt to a popcount_exprt. More...

popcount_exprt &	to_popcount_expr (exprt &expr)
	Cast an exprt to a popcount_exprt. More...

template<>
bool	can_cast_expr< binary_overflow_exprt > (const exprt &base)

void	validate_expr (const binary_overflow_exprt &value)

const binary_overflow_exprt &	to_binary_overflow_expr (const exprt &expr)
	Cast an exprt to a binary_overflow_exprt. More...

binary_overflow_exprt &	to_binary_overflow_expr (exprt &expr)
	Cast an exprt to a binary_overflow_exprt. More...

template<>
bool	can_cast_expr< plus_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< minus_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< mult_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< shl_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< unary_overflow_exprt > (const exprt &base)

void	validate_expr (const unary_overflow_exprt &value)

template<>
bool	can_cast_expr< unary_minus_overflow_exprt > (const exprt &base)

void	validate_expr (const unary_minus_overflow_exprt &value)

const unary_overflow_exprt &	to_unary_overflow_expr (const exprt &expr)
	Cast an exprt to a unary_overflow_exprt. More...

unary_overflow_exprt &	to_unary_overflow_expr (exprt &expr)
	Cast an exprt to a unary_overflow_exprt. More...

template<>
bool	can_cast_expr< count_leading_zeros_exprt > (const exprt &base)

void	validate_expr (const count_leading_zeros_exprt &value)

const count_leading_zeros_exprt &	to_count_leading_zeros_expr (const exprt &expr)
	Cast an exprt to a count_leading_zeros_exprt. More...

count_leading_zeros_exprt &	to_count_leading_zeros_expr (exprt &expr)
	Cast an exprt to a count_leading_zeros_exprt. More...

template<>
bool	can_cast_expr< count_trailing_zeros_exprt > (const exprt &base)

void	validate_expr (const count_trailing_zeros_exprt &value)

const count_trailing_zeros_exprt &	to_count_trailing_zeros_expr (const exprt &expr)
	Cast an exprt to a count_trailing_zeros_exprt. More...

count_trailing_zeros_exprt &	to_count_trailing_zeros_expr (exprt &expr)
	Cast an exprt to a count_trailing_zeros_exprt. More...

template<>
bool	can_cast_expr< bitreverse_exprt > (const exprt &base)

void	validate_expr (const bitreverse_exprt &value)

const bitreverse_exprt &	to_bitreverse_expr (const exprt &expr)
	Cast an exprt to a bitreverse_exprt. More...

bitreverse_exprt &	to_bitreverse_expr (exprt &expr)
	Cast an exprt to a bitreverse_exprt. More...

template<>
bool	can_cast_expr< saturating_plus_exprt > (const exprt &base)

void	validate_expr (const saturating_plus_exprt &value)

const saturating_plus_exprt &	to_saturating_plus_expr (const exprt &expr)
	Cast an exprt to a saturating_plus_exprt. More...

saturating_plus_exprt &	to_saturating_plus_expr (exprt &expr)
	Cast an exprt to a saturating_plus_exprt. More...

template<>
bool	can_cast_expr< saturating_minus_exprt > (const exprt &base)

void	validate_expr (const saturating_minus_exprt &value)

const saturating_minus_exprt &	to_saturating_minus_expr (const exprt &expr)
	Cast an exprt to a saturating_minus_exprt. More...

saturating_minus_exprt &	to_saturating_minus_expr (exprt &expr)
	Cast an exprt to a saturating_minus_exprt. More...

template<>
bool	can_cast_expr< overflow_result_exprt > (const exprt &base)

void	validate_expr (const overflow_result_exprt &value)

const overflow_result_exprt &	to_overflow_result_expr (const exprt &expr)
	Cast an exprt to a overflow_result_exprt. More...

overflow_result_exprt &	to_overflow_result_expr (exprt &expr)
	Cast an exprt to a overflow_result_exprt. More...

template<>
bool	can_cast_expr< find_first_set_exprt > (const exprt &base)

void	validate_expr (const find_first_set_exprt &value)

const find_first_set_exprt &	to_find_first_set_expr (const exprt &expr)
	Cast an exprt to a find_first_set_exprt. More...

find_first_set_exprt &	to_find_first_set_expr (exprt &expr)
	Cast an exprt to a find_first_set_exprt. More...

template<>
bool	can_cast_expr< zero_extend_exprt > (const exprt &base)

const zero_extend_exprt &	to_zero_extend_expr (const exprt &expr)
	Cast an exprt to a zero_extend_exprt. More...

zero_extend_exprt &	to_zero_extend_expr (exprt &expr)
	Cast an exprt to a zero_extend_exprt. More...

const onehot_exprt &	to_onehot_expr (const exprt &expr)
	Cast an exprt to a onehot_exprt. More...

onehot_exprt &	to_onehot_expr (exprt &expr)
	Cast an exprt to a onehot_exprt. More...

const onehot0_exprt &	to_onehot0_expr (const exprt &expr)
	Cast an exprt to a onehot0_exprt. More...

onehot0_exprt &	to_onehot0_expr (exprt &expr)
	Cast an exprt to a onehot0_exprt. More...

Detailed Description

API to expression classes for bitvectors.

Definition in file bitvector_expr.h.

Function Documentation

◆ can_cast_expr< ashr_exprt >()

template<>

bool can_cast_expr< ashr_exprt > ( const exprt & base )

inline

Definition at line 403 of file bitvector_expr.h.

◆ can_cast_expr< binary_overflow_exprt >()

template<>

bool can_cast_expr< binary_overflow_exprt > ( const exprt & base )

inline

Definition at line 967 of file bitvector_expr.h.

◆ can_cast_expr< bitand_exprt >()

template<>

bool can_cast_expr< bitand_exprt > ( const exprt & base )

inline

Definition at line 254 of file bitvector_expr.h.

◆ can_cast_expr< bitnot_exprt >()

template<>

bool can_cast_expr< bitnot_exprt > ( const exprt & base )

inline

Definition at line 90 of file bitvector_expr.h.

◆ can_cast_expr< bitor_exprt >()

template<>

bool can_cast_expr< bitor_exprt > ( const exprt & base )

inline

Definition at line 139 of file bitvector_expr.h.

◆ can_cast_expr< bitreverse_exprt >()

template<>

bool can_cast_expr< bitreverse_exprt > ( const exprt & base )

inline

Definition at line 1379 of file bitvector_expr.h.

◆ can_cast_expr< bitxnor_exprt >()

template<>

bool can_cast_expr< bitxnor_exprt > ( const exprt & base )

inline

Definition at line 214 of file bitvector_expr.h.

◆ can_cast_expr< bitxor_exprt >()

template<>

bool can_cast_expr< bitxor_exprt > ( const exprt & base )

inline

Definition at line 179 of file bitvector_expr.h.

◆ can_cast_expr< bswap_exprt >()

template<>

bool can_cast_expr< bswap_exprt > ( const exprt & base )

inline

Definition at line 45 of file bitvector_expr.h.

◆ can_cast_expr< concatenation_exprt >()

template<>

bool can_cast_expr< concatenation_exprt > ( const exprt & base )

inline

Definition at line 834 of file bitvector_expr.h.

◆ can_cast_expr< count_leading_zeros_exprt >()

template<>

bool can_cast_expr< count_leading_zeros_exprt > ( const exprt & base )

inline

Definition at line 1235 of file bitvector_expr.h.

◆ can_cast_expr< count_trailing_zeros_exprt >()

template<>

bool can_cast_expr< count_trailing_zeros_exprt > ( const exprt & base )

inline

Definition at line 1328 of file bitvector_expr.h.

◆ can_cast_expr< extractbit_exprt >()

template<>

bool can_cast_expr< extractbit_exprt > ( const exprt & base )

inline

Definition at line 463 of file bitvector_expr.h.

◆ can_cast_expr< extractbits_exprt >()

template<>

bool can_cast_expr< extractbits_exprt > ( const exprt & base )

inline

Definition at line 537 of file bitvector_expr.h.

◆ can_cast_expr< find_first_set_exprt >()

template<>

bool can_cast_expr< find_first_set_exprt > ( const exprt & base )

inline

Definition at line 1682 of file bitvector_expr.h.

◆ can_cast_expr< lshr_exprt >()

template<>

bool can_cast_expr< lshr_exprt > ( const exprt & base )

inline

Definition at line 424 of file bitvector_expr.h.

◆ can_cast_expr< minus_overflow_exprt >()

template<>

bool can_cast_expr< minus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1039 of file bitvector_expr.h.

◆ can_cast_expr< mult_overflow_exprt >()

template<>

bool can_cast_expr< mult_overflow_exprt > ( const exprt & base )

inline

Definition at line 1058 of file bitvector_expr.h.

◆ can_cast_expr< overflow_result_exprt >()

template<>

bool can_cast_expr< overflow_result_exprt > ( const exprt & base )

inline

Definition at line 1596 of file bitvector_expr.h.

◆ can_cast_expr< plus_overflow_exprt >()

template<>

bool can_cast_expr< plus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1020 of file bitvector_expr.h.

◆ can_cast_expr< popcount_exprt >()

template<>

bool can_cast_expr< popcount_exprt > ( const exprt & base )

inline

Definition at line 878 of file bitvector_expr.h.

◆ can_cast_expr< replication_exprt >()

template<>

bool can_cast_expr< replication_exprt > ( const exprt & base )

inline

Definition at line 778 of file bitvector_expr.h.

◆ can_cast_expr< saturating_minus_exprt >()

template<>

bool can_cast_expr< saturating_minus_exprt > ( const exprt & base )

inline

Definition at line 1477 of file bitvector_expr.h.

◆ can_cast_expr< saturating_plus_exprt >()

template<>

bool can_cast_expr< saturating_plus_exprt > ( const exprt & base )

inline

Definition at line 1432 of file bitvector_expr.h.

◆ can_cast_expr< shift_exprt >()

template<>

bool can_cast_expr< shift_exprt > ( const exprt & base )

inline

Definition at line 311 of file bitvector_expr.h.

◆ can_cast_expr< shl_exprt >()

template<>

bool can_cast_expr< shl_exprt > ( const exprt & base )

inline

Definition at line 359 of file bitvector_expr.h.

◆ can_cast_expr< shl_overflow_exprt >()

template<>

bool can_cast_expr< shl_overflow_exprt > ( const exprt & base )

inline

Definition at line 1073 of file bitvector_expr.h.

◆ can_cast_expr< unary_minus_overflow_exprt >()

template<>

bool can_cast_expr< unary_minus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1143 of file bitvector_expr.h.

◆ can_cast_expr< unary_overflow_exprt >()

template<>

bool can_cast_expr< unary_overflow_exprt > ( const exprt & base )

inline

Definition at line 1105 of file bitvector_expr.h.

◆ can_cast_expr< update_bit_exprt >()

template<>

bool can_cast_expr< update_bit_exprt > ( const exprt & base )

inline

Definition at line 631 of file bitvector_expr.h.

◆ can_cast_expr< update_bits_exprt >()

template<>

bool can_cast_expr< update_bits_exprt > ( const exprt & base )

inline

Definition at line 717 of file bitvector_expr.h.

◆ can_cast_expr< zero_extend_exprt >()

template<>

bool can_cast_expr< zero_extend_exprt > ( const exprt & base )

inline

Definition at line 1734 of file bitvector_expr.h.

◆ to_binary_overflow_expr() [1/2]

const binary_overflow_exprt& to_binary_overflow_expr ( const exprt & expr )

inline

Cast an exprt to a binary_overflow_exprt.

expr must be known to be binary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type binary_overflow_exprt

Definition at line 984 of file bitvector_expr.h.

◆ to_binary_overflow_expr() [2/2]

binary_overflow_exprt& to_binary_overflow_expr ( exprt & expr )

inline

Cast an exprt to a binary_overflow_exprt.

expr must be known to be binary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type binary_overflow_exprt

Definition at line 996 of file bitvector_expr.h.

◆ to_bitand_expr() [1/2]

const bitand_exprt& to_bitand_expr ( const exprt & expr )

inline

Cast an exprt to a bitand_exprt.

expr must be known to be bitand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitand_exprt

Definition at line 265 of file bitvector_expr.h.

◆ to_bitand_expr() [2/2]

bitand_exprt& to_bitand_expr ( exprt & expr )

inline

Cast an exprt to a bitand_exprt.

expr must be known to be bitand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitand_exprt

Definition at line 272 of file bitvector_expr.h.

◆ to_bitnot_expr() [1/2]

const bitnot_exprt& to_bitnot_expr ( const exprt & expr )

inline

Cast an exprt to a bitnot_exprt.

expr must be known to be bitnot_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnot_exprt

Definition at line 106 of file bitvector_expr.h.

◆ to_bitnot_expr() [2/2]

bitnot_exprt& to_bitnot_expr ( exprt & expr )

inline

Cast an exprt to a bitnot_exprt.

expr must be known to be bitnot_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnot_exprt

Definition at line 115 of file bitvector_expr.h.

◆ to_bitor_expr() [1/2]

const bitor_exprt& to_bitor_expr ( const exprt & expr )

inline

Cast an exprt to a bitor_exprt.

expr must be known to be bitor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitor_exprt

Definition at line 150 of file bitvector_expr.h.

◆ to_bitor_expr() [2/2]

bitor_exprt& to_bitor_expr ( exprt & expr )

inline

Cast an exprt to a bitor_exprt.

expr must be known to be bitor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitor_exprt

Definition at line 157 of file bitvector_expr.h.

◆ to_bitreverse_expr() [1/2]

const bitreverse_exprt& to_bitreverse_expr ( const exprt & expr )

inline

Cast an exprt to a bitreverse_exprt.

expr must be known to be bitreverse_exprt.

Parameters

expr	Source expression

Returns: Object of type bitreverse_exprt

Definition at line 1395 of file bitvector_expr.h.

◆ to_bitreverse_expr() [2/2]

bitreverse_exprt& to_bitreverse_expr ( exprt & expr )

inline

Cast an exprt to a bitreverse_exprt.

expr must be known to be bitreverse_exprt.

Parameters

expr	Source expression

Returns: Object of type bitreverse_exprt

Definition at line 1404 of file bitvector_expr.h.

◆ to_bitxnor_expr() [1/2]

const bitxnor_exprt& to_bitxnor_expr ( const exprt & expr )

inline

Cast an exprt to a bitxnor_exprt.

expr must be known to be bitxnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxnor_exprt

Definition at line 225 of file bitvector_expr.h.

◆ to_bitxnor_expr() [2/2]

bitxnor_exprt& to_bitxnor_expr ( exprt & expr )

inline

Cast an exprt to a bitxnor_exprt.

expr must be known to be bitxnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxnor_exprt

Definition at line 232 of file bitvector_expr.h.

◆ to_bitxor_expr() [1/2]

const bitxor_exprt& to_bitxor_expr ( const exprt & expr )

inline

Cast an exprt to a bitxor_exprt.

expr must be known to be bitxor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxor_exprt

Definition at line 190 of file bitvector_expr.h.

◆ to_bitxor_expr() [2/2]

bitxor_exprt& to_bitxor_expr ( exprt & expr )

inline

Cast an exprt to a bitxor_exprt.

expr must be known to be bitxor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxor_exprt

Definition at line 197 of file bitvector_expr.h.

◆ to_bswap_expr() [1/2]

const bswap_exprt& to_bswap_expr ( const exprt & expr )

inline

Cast an exprt to a bswap_exprt.

expr must be known to be bswap_exprt.

Parameters

expr	Source expression

Returns: Object of type bswap_exprt

Definition at line 63 of file bitvector_expr.h.

◆ to_bswap_expr() [2/2]

bswap_exprt& to_bswap_expr ( exprt & expr )

inline

Cast an exprt to a bswap_exprt.

expr must be known to be bswap_exprt.

Parameters

expr	Source expression

Returns: Object of type bswap_exprt

Definition at line 72 of file bitvector_expr.h.

◆ to_concatenation_expr() [1/2]

const concatenation_exprt& to_concatenation_expr ( const exprt & expr )

inline

Cast an exprt to a concatenation_exprt.

expr must be known to be concatenation_exprt.

Parameters

expr	Source expression

Returns: Object of type concatenation_exprt

Definition at line 845 of file bitvector_expr.h.

◆ to_concatenation_expr() [2/2]

concatenation_exprt& to_concatenation_expr ( exprt & expr )

inline

Cast an exprt to a concatenation_exprt.

expr must be known to be concatenation_exprt.

Parameters

expr	Source expression

Returns: Object of type concatenation_exprt

Definition at line 852 of file bitvector_expr.h.

◆ to_count_leading_zeros_expr() [1/2]

const count_leading_zeros_exprt& to_count_leading_zeros_expr ( const exprt & expr )

inline

Cast an exprt to a count_leading_zeros_exprt.

expr must be known to be count_leading_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_leading_zeros_exprt

Definition at line 1252 of file bitvector_expr.h.

◆ to_count_leading_zeros_expr() [2/2]

count_leading_zeros_exprt& to_count_leading_zeros_expr ( exprt & expr )

inline

Cast an exprt to a count_leading_zeros_exprt.

expr must be known to be count_leading_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_leading_zeros_exprt

Definition at line 1262 of file bitvector_expr.h.

◆ to_count_trailing_zeros_expr() [1/2]

const count_trailing_zeros_exprt& to_count_trailing_zeros_expr ( const exprt & expr )

inline

Cast an exprt to a count_trailing_zeros_exprt.

expr must be known to be count_trailing_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_trailing_zeros_exprt

Definition at line 1345 of file bitvector_expr.h.

◆ to_count_trailing_zeros_expr() [2/2]

count_trailing_zeros_exprt& to_count_trailing_zeros_expr ( exprt & expr )

inline

Cast an exprt to a count_trailing_zeros_exprt.

expr must be known to be count_trailing_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_trailing_zeros_exprt

Definition at line 1355 of file bitvector_expr.h.

◆ to_extractbit_expr() [1/2]

const extractbit_exprt& to_extractbit_expr ( const exprt & expr )

inline

Cast an exprt to an extractbit_exprt.

expr must be known to be extractbit_exprt.

Parameters

expr	Source expression

Returns: Object of type extractbit_exprt

Definition at line 479 of file bitvector_expr.h.

◆ to_extractbit_expr() [2/2]

extractbit_exprt& to_extractbit_expr ( exprt & expr )

inline

Cast an exprt to an extractbit_exprt.

expr must be known to be extractbit_exprt.

Parameters

expr	Source expression

Returns: Object of type extractbit_exprt

Definition at line 488 of file bitvector_expr.h.

◆ to_extractbits_expr() [1/2]

const extractbits_exprt& to_extractbits_expr ( const exprt & expr )

inline

Cast an exprt to an extractbits_exprt.

expr must be known to be extractbits_exprt.

Parameters

expr	Source expression

Returns: Object of type extractbits_exprt

Definition at line 553 of file bitvector_expr.h.

◆ to_extractbits_expr() [2/2]

extractbits_exprt& to_extractbits_expr ( exprt & expr )

inline

Cast an exprt to an extractbits_exprt.

expr must be known to be extractbits_exprt.

Parameters

expr	Source expression

Returns: Object of type extractbits_exprt

Definition at line 562 of file bitvector_expr.h.

◆ to_find_first_set_expr() [1/2]

const find_first_set_exprt& to_find_first_set_expr ( const exprt & expr )

inline

Cast an exprt to a find_first_set_exprt.

expr must be known to be find_first_set_exprt.

Parameters

expr	Source expression

Returns: Object of type find_first_set_exprt

Definition at line 1698 of file bitvector_expr.h.

◆ to_find_first_set_expr() [2/2]

find_first_set_exprt& to_find_first_set_expr ( exprt & expr )

inline

Cast an exprt to a find_first_set_exprt.

expr must be known to be find_first_set_exprt.

Parameters

expr	Source expression

Returns: Object of type find_first_set_exprt

Definition at line 1708 of file bitvector_expr.h.

◆ to_onehot0_expr() [1/2]

const onehot0_exprt& to_onehot0_expr ( const exprt & expr )

inline

Cast an exprt to a onehot0_exprt.

expr must be known to be onehot0_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot0_exprt

Definition at line 1815 of file bitvector_expr.h.

◆ to_onehot0_expr() [2/2]

onehot0_exprt& to_onehot0_expr ( exprt & expr )

inline

Cast an exprt to a onehot0_exprt.

expr must be known to be onehot0_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot0_exprt

Definition at line 1823 of file bitvector_expr.h.

◆ to_onehot_expr() [1/2]

const onehot_exprt& to_onehot_expr ( const exprt & expr )

inline

Cast an exprt to a onehot_exprt.

expr must be known to be onehot_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot_exprt

Definition at line 1780 of file bitvector_expr.h.

◆ to_onehot_expr() [2/2]

onehot_exprt& to_onehot_expr ( exprt & expr )

inline

Cast an exprt to a onehot_exprt.

expr must be known to be onehot_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot_exprt

Definition at line 1788 of file bitvector_expr.h.

◆ to_overflow_result_expr() [1/2]

const overflow_result_exprt& to_overflow_result_expr ( const exprt & expr )

inline

Cast an exprt to a overflow_result_exprt.

expr must be known to be overflow_result_exprt.

Parameters

expr	Source expression

Returns: Object of type overflow_result_exprt

Definition at line 1621 of file bitvector_expr.h.

◆ to_overflow_result_expr() [2/2]

overflow_result_exprt& to_overflow_result_expr ( exprt & expr )

inline

Cast an exprt to a overflow_result_exprt.

expr must be known to be overflow_result_exprt.

Parameters

expr	Source expression

Returns: Object of type overflow_result_exprt

Definition at line 1631 of file bitvector_expr.h.

◆ to_popcount_expr() [1/2]

const popcount_exprt& to_popcount_expr ( const exprt & expr )

inline

Cast an exprt to a popcount_exprt.

expr must be known to be popcount_exprt.

Parameters

expr	Source expression

Returns: Object of type popcount_exprt

Definition at line 894 of file bitvector_expr.h.

◆ to_popcount_expr() [2/2]

popcount_exprt& to_popcount_expr ( exprt & expr )

inline

Cast an exprt to a popcount_exprt.

expr must be known to be popcount_exprt.

Parameters

expr	Source expression

Returns: Object of type popcount_exprt

Definition at line 903 of file bitvector_expr.h.

◆ to_replication_expr() [1/2]

const replication_exprt& to_replication_expr ( const exprt & expr )

inline

Cast an exprt to a replication_exprt.

expr must be known to be replication_exprt.

Parameters

expr	Source expression

Returns: Object of type replication_exprt

Definition at line 794 of file bitvector_expr.h.

◆ to_replication_expr() [2/2]

replication_exprt& to_replication_expr ( exprt & expr )

inline

Cast an exprt to a replication_exprt.

expr must be known to be replication_exprt.

Parameters

expr	Source expression

Returns: Object of type replication_exprt

Definition at line 803 of file bitvector_expr.h.

◆ to_saturating_minus_expr() [1/2]

const saturating_minus_exprt& to_saturating_minus_expr ( const exprt & expr )

inline

Cast an exprt to a saturating_minus_exprt.

expr must be known to be saturating_minus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_minus_exprt

Definition at line 1493 of file bitvector_expr.h.

◆ to_saturating_minus_expr() [2/2]

saturating_minus_exprt& to_saturating_minus_expr ( exprt & expr )

inline

Cast an exprt to a saturating_minus_exprt.

expr must be known to be saturating_minus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_minus_exprt

Definition at line 1503 of file bitvector_expr.h.

◆ to_saturating_plus_expr() [1/2]

const saturating_plus_exprt& to_saturating_plus_expr ( const exprt & expr )

inline

Cast an exprt to a saturating_plus_exprt.

expr must be known to be saturating_plus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_plus_exprt

Definition at line 1448 of file bitvector_expr.h.

◆ to_saturating_plus_expr() [2/2]

saturating_plus_exprt& to_saturating_plus_expr ( exprt & expr )

inline

Cast an exprt to a saturating_plus_exprt.

expr must be known to be saturating_plus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_plus_exprt

Definition at line 1458 of file bitvector_expr.h.

◆ to_shift_expr() [1/2]

const shift_exprt& to_shift_expr ( const exprt & expr )

inline

Cast an exprt to a shift_exprt.

expr must be known to be shift_exprt.

Parameters

expr	Source expression

Returns: Object of type shift_exprt

Definition at line 328 of file bitvector_expr.h.

◆ to_shift_expr() [2/2]

shift_exprt& to_shift_expr ( exprt & expr )

inline

Cast an exprt to a shift_exprt.

expr must be known to be shift_exprt.

Parameters

expr	Source expression

Returns: Object of type shift_exprt

Definition at line 336 of file bitvector_expr.h.

◆ to_shl_expr() [1/2]

const shl_exprt& to_shl_expr ( const exprt & expr )

inline

Cast an exprt to a shl_exprt.

expr must be known to be shl_exprt.

Parameters

expr	Source expression

Returns: Object of type shl_exprt

Definition at line 370 of file bitvector_expr.h.

◆ to_shl_expr() [2/2]

shl_exprt& to_shl_expr ( exprt & expr )

inline

Cast an exprt to a shl_exprt.

expr must be known to be shl_exprt.

Parameters

expr	Source expression

Returns: Object of type shl_exprt

Definition at line 379 of file bitvector_expr.h.

◆ to_unary_overflow_expr() [1/2]

const unary_overflow_exprt& to_unary_overflow_expr ( const exprt & expr )

inline

Cast an exprt to a unary_overflow_exprt.

expr must be known to be unary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type unary_overflow_exprt

Definition at line 1160 of file bitvector_expr.h.

◆ to_unary_overflow_expr() [2/2]

unary_overflow_exprt& to_unary_overflow_expr ( exprt & expr )

inline

Cast an exprt to a unary_overflow_exprt.

expr must be known to be unary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type unary_overflow_exprt

Definition at line 1170 of file bitvector_expr.h.

◆ to_update_bit_expr() [1/2]

const update_bit_exprt& to_update_bit_expr ( const exprt & expr )

inline

Cast an exprt to an update_bit_exprt.

expr must be known to be update_bit_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bit_exprt

Definition at line 642 of file bitvector_expr.h.

◆ to_update_bit_expr() [2/2]

update_bit_exprt& to_update_bit_expr ( exprt & expr )

inline

Cast an exprt to an update_bit_exprt.

expr must be known to be update_bit_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bit_exprt

Definition at line 650 of file bitvector_expr.h.

◆ to_update_bits_expr() [1/2]

const update_bits_exprt& to_update_bits_expr ( const exprt & expr )

inline

Cast an exprt to an update_bits_exprt.

expr must be known to be update_bits_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bits_exprt

Definition at line 728 of file bitvector_expr.h.

◆ to_update_bits_expr() [2/2]

update_bits_exprt& to_update_bits_expr ( exprt & expr )

inline

Cast an exprt to an update_bits_exprt.

expr must be known to be update_bits_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bits_exprt

Definition at line 736 of file bitvector_expr.h.

◆ to_zero_extend_expr() [1/2]

const zero_extend_exprt& to_zero_extend_expr ( const exprt & expr )

inline

Cast an exprt to a zero_extend_exprt.

expr must be known to be zero_extend_exprt.

Parameters

expr	Source expression

Returns: Object of type zero_extend_exprt

Definition at line 1745 of file bitvector_expr.h.

◆ to_zero_extend_expr() [2/2]

zero_extend_exprt& to_zero_extend_expr ( exprt & expr )

inline

Cast an exprt to a zero_extend_exprt.

expr must be known to be zero_extend_exprt.

Parameters

expr	Source expression

Returns: Object of type zero_extend_exprt

Definition at line 1753 of file bitvector_expr.h.

◆ validate_expr() [1/17]

void validate_expr ( const binary_overflow_exprt & value )

inline

Definition at line 972 of file bitvector_expr.h.

◆ validate_expr() [2/17]

void validate_expr ( const bitnot_exprt & value )

inline

Definition at line 95 of file bitvector_expr.h.

◆ validate_expr() [3/17]

void validate_expr ( const bitreverse_exprt & value )

inline

Definition at line 1384 of file bitvector_expr.h.

◆ validate_expr() [4/17]

void validate_expr ( const bswap_exprt & value )

inline

Definition at line 50 of file bitvector_expr.h.

◆ validate_expr() [5/17]

void validate_expr ( const count_leading_zeros_exprt & value )

inline

Definition at line 1240 of file bitvector_expr.h.

◆ validate_expr() [6/17]

void validate_expr ( const count_trailing_zeros_exprt & value )

inline

Definition at line 1333 of file bitvector_expr.h.

◆ validate_expr() [7/17]

void validate_expr ( const extractbit_exprt & value )

inline

Definition at line 468 of file bitvector_expr.h.

◆ validate_expr() [8/17]

void validate_expr ( const extractbits_exprt & value )

inline

Definition at line 542 of file bitvector_expr.h.

◆ validate_expr() [9/17]

void validate_expr ( const find_first_set_exprt & value )

inline

Definition at line 1687 of file bitvector_expr.h.

◆ validate_expr() [10/17]

void validate_expr ( const overflow_result_exprt & value )

inline

Definition at line 1601 of file bitvector_expr.h.

◆ validate_expr() [11/17]

void validate_expr ( const popcount_exprt & value )

inline

Definition at line 883 of file bitvector_expr.h.

◆ validate_expr() [12/17]

void validate_expr ( const replication_exprt & value )

inline

Definition at line 783 of file bitvector_expr.h.

◆ validate_expr() [13/17]

void validate_expr ( const saturating_minus_exprt & value )

inline

Definition at line 1482 of file bitvector_expr.h.

◆ validate_expr() [14/17]

void validate_expr ( const saturating_plus_exprt & value )

inline

Definition at line 1437 of file bitvector_expr.h.

◆ validate_expr() [15/17]

void validate_expr ( const shift_exprt & value )

inline

Definition at line 317 of file bitvector_expr.h.

◆ validate_expr() [16/17]

void validate_expr ( const unary_minus_overflow_exprt & value )

inline

Definition at line 1148 of file bitvector_expr.h.

◆ validate_expr() [17/17]

void validate_expr ( const unary_overflow_exprt & value )

inline

Definition at line 1110 of file bitvector_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_expr< ashr_exprt >()

◆ can_cast_expr< binary_overflow_exprt >()

◆ can_cast_expr< bitand_exprt >()

◆ can_cast_expr< bitnot_exprt >()

◆ can_cast_expr< bitor_exprt >()

◆ can_cast_expr< bitreverse_exprt >()

◆ can_cast_expr< bitxnor_exprt >()

◆ can_cast_expr< bitxor_exprt >()

◆ can_cast_expr< bswap_exprt >()

◆ can_cast_expr< concatenation_exprt >()

◆ can_cast_expr< count_leading_zeros_exprt >()

◆ can_cast_expr< count_trailing_zeros_exprt >()

◆ can_cast_expr< extractbit_exprt >()

◆ can_cast_expr< extractbits_exprt >()

◆ can_cast_expr< find_first_set_exprt >()

◆ can_cast_expr< lshr_exprt >()

◆ can_cast_expr< minus_overflow_exprt >()

◆ can_cast_expr< mult_overflow_exprt >()

◆ can_cast_expr< overflow_result_exprt >()

◆ can_cast_expr< plus_overflow_exprt >()

◆ can_cast_expr< popcount_exprt >()

◆ can_cast_expr< replication_exprt >()

◆ can_cast_expr< saturating_minus_exprt >()

◆ can_cast_expr< saturating_plus_exprt >()

◆ can_cast_expr< shift_exprt >()

◆ can_cast_expr< shl_exprt >()

◆ can_cast_expr< shl_overflow_exprt >()

◆ can_cast_expr< unary_minus_overflow_exprt >()

◆ can_cast_expr< unary_overflow_exprt >()

◆ can_cast_expr< update_bit_exprt >()

◆ can_cast_expr< update_bits_exprt >()

◆ can_cast_expr< zero_extend_exprt >()

◆ to_binary_overflow_expr() [1/2]

◆ to_binary_overflow_expr() [2/2]

◆ to_bitand_expr() [1/2]

◆ to_bitand_expr() [2/2]

◆ to_bitnot_expr() [1/2]

◆ to_bitnot_expr() [2/2]

◆ to_bitor_expr() [1/2]

◆ to_bitor_expr() [2/2]

◆ to_bitreverse_expr() [1/2]

◆ to_bitreverse_expr() [2/2]

◆ to_bitxnor_expr() [1/2]

◆ to_bitxnor_expr() [2/2]

◆ to_bitxor_expr() [1/2]

◆ to_bitxor_expr() [2/2]

◆ to_bswap_expr() [1/2]

◆ to_bswap_expr() [2/2]

◆ to_concatenation_expr() [1/2]

◆ to_concatenation_expr() [2/2]

◆ to_count_leading_zeros_expr() [1/2]

◆ to_count_leading_zeros_expr() [2/2]

◆ to_count_trailing_zeros_expr() [1/2]

◆ to_count_trailing_zeros_expr() [2/2]

◆ to_extractbit_expr() [1/2]

◆ to_extractbit_expr() [2/2]

◆ to_extractbits_expr() [1/2]

◆ to_extractbits_expr() [2/2]

◆ to_find_first_set_expr() [1/2]

◆ to_find_first_set_expr() [2/2]

◆ to_onehot0_expr() [1/2]

◆ to_onehot0_expr() [2/2]

◆ to_onehot_expr() [1/2]

◆ to_onehot_expr() [2/2]

◆ to_overflow_result_expr() [1/2]

◆ to_overflow_result_expr() [2/2]

◆ to_popcount_expr() [1/2]

◆ to_popcount_expr() [2/2]

◆ to_replication_expr() [1/2]

◆ to_replication_expr() [2/2]

◆ to_saturating_minus_expr() [1/2]

◆ to_saturating_minus_expr() [2/2]

◆ to_saturating_plus_expr() [1/2]

◆ to_saturating_plus_expr() [2/2]

◆ to_shift_expr() [1/2]

◆ to_shift_expr() [2/2]