API to expression classes for bitvectors. More...

#include "bitvector_types.h"
#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 Any number of operands that is greater or equal one. More...

class	bitnor_exprt
	Bit-wise NOR. More...

class	bitxor_exprt
	Bit-wise XOR Any number of operands that is greater or equal one. More...

class	bitxnor_exprt
	Bit-wise XNOR. More...

class	bitand_exprt
	Bit-wise AND Any number of operands that is greater or equal one. More...

class	bitnand_exprt
	Bit-wise NAND. 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...

class	reduction_and_exprt
	Boolean reduction: true iff every bit of the operand is `1`. More...

class	reduction_or_exprt
	Boolean reduction: true iff any bit of the operand is `1`. More...

class	reduction_nor_exprt
	Boolean reduction: negation of reduction_or_exprt. More...

class	reduction_nand_exprt
	Boolean reduction: negation of reduction_and_exprt. More...

class	reduction_xor_exprt
	Boolean reduction: XOR (parity) of all bits in the operand. More...

class	reduction_xnor_exprt
	Boolean reduction: negation of reduction_xor_exprt. 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.

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

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.

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

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.

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

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

const bitnor_exprt &	to_bitnor_expr (const exprt &expr)
	Cast an exprt to a bitnor_exprt.

bitnor_exprt &	to_bitnor_expr (exprt &expr)
	Cast an exprt to a bitnor_exprt.

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.

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

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.

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

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.

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

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

const bitnand_exprt &	to_bitnand_expr (const exprt &expr)
	Cast an exprt to a bitnand_exprt.

bitnand_exprt &	to_bitnand_expr (exprt &expr)
	Cast an exprt to a bitnand_exprt.

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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

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

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

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

template<>
bool	can_cast_expr< reduction_and_exprt > (const exprt &expr)

const reduction_and_exprt &	to_reduction_and_expr (const exprt &expr)
	Cast an exprt to a reduction_and_exprt.

reduction_and_exprt &	to_reduction_and_expr (exprt &expr)
	Cast an exprt to a reduction_and_exprt.

template<>
bool	can_cast_expr< reduction_or_exprt > (const exprt &expr)

const reduction_or_exprt &	to_reduction_or_expr (const exprt &expr)
	Cast an exprt to a reduction_or_exprt.

reduction_or_exprt &	to_reduction_or_expr (exprt &expr)
	Cast an exprt to a reduction_or_exprt.

template<>
bool	can_cast_expr< reduction_nor_exprt > (const exprt &expr)

const reduction_nor_exprt &	to_reduction_nor_expr (const exprt &expr)
	Cast an exprt to a reduction_nor_exprt.

reduction_nor_exprt &	to_reduction_nor_expr (exprt &expr)
	Cast an exprt to a reduction_nor_exprt.

template<>
bool	can_cast_expr< reduction_nand_exprt > (const exprt &expr)

const reduction_nand_exprt &	to_reduction_nand_expr (const exprt &expr)
	Cast an exprt to a reduction_nand_exprt.

reduction_nand_exprt &	to_reduction_nand_expr (exprt &expr)
	Cast an exprt to a reduction_nand_exprt.

template<>
bool	can_cast_expr< reduction_xor_exprt > (const exprt &expr)

const reduction_xor_exprt &	to_reduction_xor_expr (const exprt &expr)
	Cast an exprt to a reduction_xor_exprt.

reduction_xor_exprt &	to_reduction_xor_expr (exprt &expr)
	Cast an exprt to a reduction_xor_exprt.

template<>
bool	can_cast_expr< reduction_xnor_exprt > (const exprt &expr)

const reduction_xnor_exprt &	to_reduction_xnor_expr (const exprt &expr)
	Cast an exprt to a reduction_xnor_exprt.

reduction_xnor_exprt &	to_reduction_xnor_expr (exprt &expr)
	Cast an exprt to a reduction_xnor_exprt.

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 545 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 1110 of file bitvector_expr.h.

◆ can_cast_expr< bitand_exprt >()

template<>

bool can_cast_expr< bitand_exprt > ( const exprt & base )

inline

Definition at line 345 of file bitvector_expr.h.

◆ can_cast_expr< bitnand_exprt >()

template<>

bool can_cast_expr< bitnand_exprt > ( const exprt & base )

inline

Definition at line 396 of file bitvector_expr.h.

◆ can_cast_expr< bitnor_exprt >()

template<>

bool can_cast_expr< bitnor_exprt > ( const exprt & base )

inline

Definition at line 198 of file bitvector_expr.h.

◆ can_cast_expr< bitnot_exprt >()

template<>

bool can_cast_expr< bitnot_exprt > ( const exprt & base )

inline

Definition at line 91 of file bitvector_expr.h.

◆ can_cast_expr< bitor_exprt >()

template<>

bool can_cast_expr< bitor_exprt > ( const exprt & base )

inline

Definition at line 147 of file bitvector_expr.h.

◆ can_cast_expr< bitreverse_exprt >()

template<>

bool can_cast_expr< bitreverse_exprt > ( const exprt & base )

inline

Definition at line 1522 of file bitvector_expr.h.

◆ can_cast_expr< bitxnor_exprt >()

template<>

bool can_cast_expr< bitxnor_exprt > ( const exprt & base )

inline

Definition at line 296 of file bitvector_expr.h.

◆ can_cast_expr< bitxor_exprt >()

template<>

bool can_cast_expr< bitxor_exprt > ( const exprt & base )

inline

Definition at line 245 of file bitvector_expr.h.

◆ can_cast_expr< bswap_exprt >()

template<>

bool can_cast_expr< bswap_exprt > ( const exprt & base )

inline

Definition at line 46 of file bitvector_expr.h.

◆ can_cast_expr< concatenation_exprt >()

template<>

bool can_cast_expr< concatenation_exprt > ( const exprt & base )

inline

Definition at line 977 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 1378 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 1471 of file bitvector_expr.h.

◆ can_cast_expr< extractbit_exprt >()

template<>

bool can_cast_expr< extractbit_exprt > ( const exprt & base )

inline

Definition at line 605 of file bitvector_expr.h.

◆ can_cast_expr< extractbits_exprt >()

template<>

bool can_cast_expr< extractbits_exprt > ( const exprt & base )

inline

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

◆ can_cast_expr< lshr_exprt >()

template<>

bool can_cast_expr< lshr_exprt > ( const exprt & base )

inline

Definition at line 566 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 1182 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 1201 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 1739 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 1163 of file bitvector_expr.h.

◆ can_cast_expr< popcount_exprt >()

template<>

bool can_cast_expr< popcount_exprt > ( const exprt & base )

inline

Definition at line 1021 of file bitvector_expr.h.

◆ can_cast_expr< reduction_and_exprt >()

template<>

bool can_cast_expr< reduction_and_exprt > ( const exprt & expr )

inline

Definition at line 1984 of file bitvector_expr.h.

◆ can_cast_expr< reduction_nand_exprt >()

template<>

bool can_cast_expr< reduction_nand_exprt > ( const exprt & expr )

inline

Definition at line 2095 of file bitvector_expr.h.

◆ can_cast_expr< reduction_nor_exprt >()

template<>

bool can_cast_expr< reduction_nor_exprt > ( const exprt & expr )

inline

Definition at line 2058 of file bitvector_expr.h.

◆ can_cast_expr< reduction_or_exprt >()

template<>

bool can_cast_expr< reduction_or_exprt > ( const exprt & expr )

inline

Definition at line 2021 of file bitvector_expr.h.

◆ can_cast_expr< reduction_xnor_exprt >()

template<>

bool can_cast_expr< reduction_xnor_exprt > ( const exprt & expr )

inline

Definition at line 2169 of file bitvector_expr.h.

◆ can_cast_expr< reduction_xor_exprt >()

template<>

bool can_cast_expr< reduction_xor_exprt > ( const exprt & expr )

inline

Definition at line 2132 of file bitvector_expr.h.

◆ can_cast_expr< replication_exprt >()

template<>

bool can_cast_expr< replication_exprt > ( const exprt & base )

inline

Definition at line 920 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 1620 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 1575 of file bitvector_expr.h.

◆ can_cast_expr< shift_exprt >()

template<>

bool can_cast_expr< shift_exprt > ( const exprt & base )

inline

Definition at line 453 of file bitvector_expr.h.

◆ can_cast_expr< shl_exprt >()

template<>

bool can_cast_expr< shl_exprt > ( const exprt & base )

inline

Definition at line 501 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 1216 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 1286 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 1248 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 773 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 859 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 1877 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 1127 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 1139 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 356 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 363 of file bitvector_expr.h.

◆ to_bitnand_expr() [1/2]

const bitnand_exprt & to_bitnand_expr ( const exprt & expr )

inline

Cast an exprt to a bitnand_exprt.

expr must be known to be bitnand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnand_exprt

Definition at line 407 of file bitvector_expr.h.

◆ to_bitnand_expr() [2/2]

bitnand_exprt & to_bitnand_expr ( exprt & expr )

inline

Cast an exprt to a bitnand_exprt.

expr must be known to be bitnand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnand_exprt

Definition at line 414 of file bitvector_expr.h.

◆ to_bitnor_expr() [1/2]

const bitnor_exprt & to_bitnor_expr ( const exprt & expr )

inline

Cast an exprt to a bitnor_exprt.

expr must be known to be bitnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnor_exprt

Definition at line 209 of file bitvector_expr.h.

◆ to_bitnor_expr() [2/2]

bitnor_exprt & to_bitnor_expr ( exprt & expr )

inline

Cast an exprt to a bitnor_exprt.

expr must be known to be bitnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnor_exprt

Definition at line 216 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 107 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 116 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 158 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 165 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 1538 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 1547 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 307 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 315 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 256 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 263 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 64 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 73 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 988 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 995 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 1395 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 1405 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 1488 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 1498 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 621 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 630 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 695 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 704 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 1841 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 1851 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 1958 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 1966 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 1923 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 1931 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 1764 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 1774 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 1037 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 1046 of file bitvector_expr.h.

◆ to_reduction_and_expr() [1/2]

const reduction_and_exprt & to_reduction_and_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_and_exprt.

expr must be known to be reduction_and_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_and_exprt

Definition at line 1995 of file bitvector_expr.h.

◆ to_reduction_and_expr() [2/2]

reduction_and_exprt & to_reduction_and_expr ( exprt & expr )

inline

Cast an exprt to a reduction_and_exprt.

expr must be known to be reduction_and_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_and_exprt

Definition at line 2003 of file bitvector_expr.h.

◆ to_reduction_nand_expr() [1/2]

const reduction_nand_exprt & to_reduction_nand_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_nand_exprt.

expr must be known to be reduction_nand_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_nand_exprt

Definition at line 2106 of file bitvector_expr.h.

◆ to_reduction_nand_expr() [2/2]

reduction_nand_exprt & to_reduction_nand_expr ( exprt & expr )

inline

Cast an exprt to a reduction_nand_exprt.

expr must be known to be reduction_nand_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_nand_exprt

Definition at line 2114 of file bitvector_expr.h.

◆ to_reduction_nor_expr() [1/2]

const reduction_nor_exprt & to_reduction_nor_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_nor_exprt.

expr must be known to be reduction_nor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_nor_exprt

Definition at line 2069 of file bitvector_expr.h.

◆ to_reduction_nor_expr() [2/2]

reduction_nor_exprt & to_reduction_nor_expr ( exprt & expr )

inline

Cast an exprt to a reduction_nor_exprt.

expr must be known to be reduction_nor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_nor_exprt

Definition at line 2077 of file bitvector_expr.h.

◆ to_reduction_or_expr() [1/2]

const reduction_or_exprt & to_reduction_or_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_or_exprt.

expr must be known to be reduction_or_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_or_exprt

Definition at line 2032 of file bitvector_expr.h.

◆ to_reduction_or_expr() [2/2]

reduction_or_exprt & to_reduction_or_expr ( exprt & expr )

inline

Cast an exprt to a reduction_or_exprt.

expr must be known to be reduction_or_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_or_exprt

Definition at line 2040 of file bitvector_expr.h.

◆ to_reduction_xnor_expr() [1/2]

const reduction_xnor_exprt & to_reduction_xnor_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_xnor_exprt.

expr must be known to be reduction_xnor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_xnor_exprt

Definition at line 2180 of file bitvector_expr.h.

◆ to_reduction_xnor_expr() [2/2]

reduction_xnor_exprt & to_reduction_xnor_expr ( exprt & expr )

inline

Cast an exprt to a reduction_xnor_exprt.

expr must be known to be reduction_xnor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_xnor_exprt

Definition at line 2188 of file bitvector_expr.h.

◆ to_reduction_xor_expr() [1/2]

const reduction_xor_exprt & to_reduction_xor_expr ( const exprt & expr )

inline

Cast an exprt to a reduction_xor_exprt.

expr must be known to be reduction_xor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_xor_exprt

Definition at line 2143 of file bitvector_expr.h.

◆ to_reduction_xor_expr() [2/2]

reduction_xor_exprt & to_reduction_xor_expr ( exprt & expr )

inline

Cast an exprt to a reduction_xor_exprt.

expr must be known to be reduction_xor_exprt.

Parameters

expr	Source expression

Returns: Object of type reduction_xor_exprt

Definition at line 2151 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 936 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 945 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 1636 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 1646 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 1591 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 1601 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 470 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 478 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 512 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 521 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 1303 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 1313 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 784 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 792 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 870 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 878 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 1888 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 1896 of file bitvector_expr.h.

◆ validate_expr() [1/17]

void validate_expr ( const binary_overflow_exprt & value )

inline

Definition at line 1115 of file bitvector_expr.h.

◆ validate_expr() [2/17]

void validate_expr ( const bitnot_exprt & value )

inline

Definition at line 96 of file bitvector_expr.h.

◆ validate_expr() [3/17]

void validate_expr ( const bitreverse_exprt & value )

inline

Definition at line 1527 of file bitvector_expr.h.

◆ validate_expr() [4/17]

void validate_expr ( const bswap_exprt & value )

inline

Definition at line 51 of file bitvector_expr.h.

◆ validate_expr() [5/17]

void validate_expr ( const count_leading_zeros_exprt & value )

inline

Definition at line 1383 of file bitvector_expr.h.

◆ validate_expr() [6/17]

void validate_expr ( const count_trailing_zeros_exprt & value )

inline

Definition at line 1476 of file bitvector_expr.h.

◆ validate_expr() [7/17]

void validate_expr ( const extractbit_exprt & value )

inline

Definition at line 610 of file bitvector_expr.h.

◆ validate_expr() [8/17]

void validate_expr ( const extractbits_exprt & value )

inline

Definition at line 684 of file bitvector_expr.h.

◆ validate_expr() [9/17]

void validate_expr ( const find_first_set_exprt & value )

inline

Definition at line 1830 of file bitvector_expr.h.

◆ validate_expr() [10/17]

void validate_expr ( const overflow_result_exprt & value )

inline

Definition at line 1744 of file bitvector_expr.h.

◆ validate_expr() [11/17]

void validate_expr ( const popcount_exprt & value )

inline

Definition at line 1026 of file bitvector_expr.h.

◆ validate_expr() [12/17]

void validate_expr ( const replication_exprt & value )

inline

Definition at line 925 of file bitvector_expr.h.

◆ validate_expr() [13/17]

void validate_expr ( const saturating_minus_exprt & value )

inline

Definition at line 1625 of file bitvector_expr.h.

◆ validate_expr() [14/17]

void validate_expr ( const saturating_plus_exprt & value )

inline

Definition at line 1580 of file bitvector_expr.h.

◆ validate_expr() [15/17]

void validate_expr ( const shift_exprt & value )

inline

Definition at line 459 of file bitvector_expr.h.

◆ validate_expr() [16/17]

void validate_expr ( const unary_minus_overflow_exprt & value )

inline

Definition at line 1291 of file bitvector_expr.h.

◆ validate_expr() [17/17]

void validate_expr ( const unary_overflow_exprt & value )

inline

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

◆ can_cast_expr< bitnor_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< reduction_and_exprt >()

◆ can_cast_expr< reduction_nand_exprt >()

◆ can_cast_expr< reduction_nor_exprt >()

◆ can_cast_expr< reduction_or_exprt >()

◆ can_cast_expr< reduction_xnor_exprt >()

◆ can_cast_expr< reduction_xor_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_bitnand_expr() [1/2]

◆ to_bitnand_expr() [2/2]

◆ to_bitnor_expr() [1/2]

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