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

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

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 353 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 931 of file bitvector_expr.h.

◆ can_cast_expr< bitand_exprt >()

template<>

bool can_cast_expr< bitand_exprt > ( const exprt & base )

inline

Definition at line 204 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 134 of file bitvector_expr.h.

◆ can_cast_expr< bitreverse_exprt >()

template<>

bool can_cast_expr< bitreverse_exprt > ( const exprt & base )

inline

Definition at line 1343 of file bitvector_expr.h.

◆ can_cast_expr< bitxor_exprt >()

template<>

bool can_cast_expr< bitxor_exprt > ( const exprt & base )

inline

Definition at line 169 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 798 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 1199 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 1292 of file bitvector_expr.h.

◆ can_cast_expr< extractbit_exprt >()

template<>

bool can_cast_expr< extractbit_exprt > ( const exprt & base )

inline

Definition at line 413 of file bitvector_expr.h.

◆ can_cast_expr< extractbits_exprt >()

template<>

bool can_cast_expr< extractbits_exprt > ( const exprt & base )

inline

Definition at line 501 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 1646 of file bitvector_expr.h.

◆ can_cast_expr< lshr_exprt >()

template<>

bool can_cast_expr< lshr_exprt > ( const exprt & base )

inline

Definition at line 374 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 1003 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 1022 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 1560 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 984 of file bitvector_expr.h.

◆ can_cast_expr< popcount_exprt >()

template<>

bool can_cast_expr< popcount_exprt > ( const exprt & base )

inline

Definition at line 842 of file bitvector_expr.h.

◆ can_cast_expr< replication_exprt >()

template<>

bool can_cast_expr< replication_exprt > ( const exprt & base )

inline

Definition at line 742 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 1441 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 1396 of file bitvector_expr.h.

◆ can_cast_expr< shift_exprt >()

template<>

bool can_cast_expr< shift_exprt > ( const exprt & base )

inline

Definition at line 261 of file bitvector_expr.h.

◆ can_cast_expr< shl_exprt >()

template<>

bool can_cast_expr< shl_exprt > ( const exprt & base )

inline

Definition at line 309 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 1037 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 1107 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 1069 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 595 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 681 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 948 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 960 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 215 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 222 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 145 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 152 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 1359 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 1368 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 180 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 187 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 809 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 816 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 1216 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 1226 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 1309 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 1319 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 429 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 438 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 517 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 526 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 1662 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 1672 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 1585 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 1595 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 858 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 867 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 758 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 767 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 1457 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 1467 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 1412 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 1422 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 278 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 286 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 320 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 329 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 1124 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 1134 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 606 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 614 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 692 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 700 of file bitvector_expr.h.

◆ validate_expr() [1/17]

void validate_expr ( const binary_overflow_exprt & value )

inline

Definition at line 936 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 1348 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 1204 of file bitvector_expr.h.

◆ validate_expr() [6/17]

void validate_expr ( const count_trailing_zeros_exprt & value )

inline

Definition at line 1297 of file bitvector_expr.h.

◆ validate_expr() [7/17]

void validate_expr ( const extractbit_exprt & value )

inline

Definition at line 418 of file bitvector_expr.h.

◆ validate_expr() [8/17]

void validate_expr ( const extractbits_exprt & value )

inline

Definition at line 506 of file bitvector_expr.h.

◆ validate_expr() [9/17]

void validate_expr ( const find_first_set_exprt & value )

inline

Definition at line 1651 of file bitvector_expr.h.

◆ validate_expr() [10/17]

void validate_expr ( const overflow_result_exprt & value )

inline

Definition at line 1565 of file bitvector_expr.h.

◆ validate_expr() [11/17]

void validate_expr ( const popcount_exprt & value )

inline

Definition at line 847 of file bitvector_expr.h.

◆ validate_expr() [12/17]

void validate_expr ( const replication_exprt & value )

inline

Definition at line 747 of file bitvector_expr.h.

◆ validate_expr() [13/17]

void validate_expr ( const saturating_minus_exprt & value )

inline

Definition at line 1446 of file bitvector_expr.h.

◆ validate_expr() [14/17]

void validate_expr ( const saturating_plus_exprt & value )

inline

Definition at line 1401 of file bitvector_expr.h.

◆ validate_expr() [15/17]

void validate_expr ( const shift_exprt & value )

inline

Definition at line 267 of file bitvector_expr.h.

◆ validate_expr() [16/17]

void validate_expr ( const unary_minus_overflow_exprt & value )

inline

Definition at line 1112 of file bitvector_expr.h.

◆ validate_expr() [17/17]

void validate_expr ( const unary_overflow_exprt & value )

inline

Definition at line 1074 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< 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 >()

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

◆ to_shl_expr() [1/2]

◆ to_shl_expr() [2/2]

◆ to_unary_overflow_expr() [1/2]

◆ to_unary_overflow_expr() [2/2]

◆ to_update_bit_expr() [1/2]

◆ to_update_bit_expr() [2/2]

◆ to_update_bits_expr() [1/2]

◆ to_update_bits_expr() [2/2]