CBMC
bitvector_expr.h File Reference

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:

Go to the source code of 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_exprtto_bswap_expr (const exprt &expr)
 Cast an exprt to a bswap_exprt. More...
 
bswap_exprtto_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_exprtto_bitnot_expr (const exprt &expr)
 Cast an exprt to a bitnot_exprt. More...
 
bitnot_exprtto_bitnot_expr (exprt &expr)
 Cast an exprt to a bitnot_exprt. More...
 
template<>
bool can_cast_expr< bitor_exprt > (const exprt &base)
 
const bitor_exprtto_bitor_expr (const exprt &expr)
 Cast an exprt to a bitor_exprt. More...
 
bitor_exprtto_bitor_expr (exprt &expr)
 Cast an exprt to a bitor_exprt. More...
 
template<>
bool can_cast_expr< bitxor_exprt > (const exprt &base)
 
const bitxor_exprtto_bitxor_expr (const exprt &expr)
 Cast an exprt to a bitxor_exprt. More...
 
bitxor_exprtto_bitxor_expr (exprt &expr)
 Cast an exprt to a bitxor_exprt. More...
 
template<>
bool can_cast_expr< bitxnor_exprt > (const exprt &base)
 
const bitxnor_exprtto_bitxnor_expr (const exprt &expr)
 Cast an exprt to a bitxnor_exprt. More...
 
bitxnor_exprtto_bitxnor_expr (exprt &expr)
 Cast an exprt to a bitxnor_exprt. More...
 
template<>
bool can_cast_expr< bitand_exprt > (const exprt &base)
 
const bitand_exprtto_bitand_expr (const exprt &expr)
 Cast an exprt to a bitand_exprt. More...
 
bitand_exprtto_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_exprtto_shift_expr (const exprt &expr)
 Cast an exprt to a shift_exprt. More...
 
shift_exprtto_shift_expr (exprt &expr)
 Cast an exprt to a shift_exprt. More...
 
template<>
bool can_cast_expr< shl_exprt > (const exprt &base)
 
const shl_exprtto_shl_expr (const exprt &expr)
 Cast an exprt to a shl_exprt. More...
 
shl_exprtto_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_exprtto_extractbit_expr (const exprt &expr)
 Cast an exprt to an extractbit_exprt. More...
 
extractbit_exprtto_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_exprtto_extractbits_expr (const exprt &expr)
 Cast an exprt to an extractbits_exprt. More...
 
extractbits_exprtto_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_exprtto_update_bit_expr (const exprt &expr)
 Cast an exprt to an update_bit_exprt. More...
 
update_bit_exprtto_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_exprtto_update_bits_expr (const exprt &expr)
 Cast an exprt to an update_bits_exprt. More...
 
update_bits_exprtto_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_exprtto_replication_expr (const exprt &expr)
 Cast an exprt to a replication_exprt. More...
 
replication_exprtto_replication_expr (exprt &expr)
 Cast an exprt to a replication_exprt. More...
 
template<>
bool can_cast_expr< concatenation_exprt > (const exprt &base)
 
const concatenation_exprtto_concatenation_expr (const exprt &expr)
 Cast an exprt to a concatenation_exprt. More...
 
concatenation_exprtto_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_exprtto_popcount_expr (const exprt &expr)
 Cast an exprt to a popcount_exprt. More...
 
popcount_exprtto_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_exprtto_binary_overflow_expr (const exprt &expr)
 Cast an exprt to a binary_overflow_exprt. More...
 
binary_overflow_exprtto_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_exprtto_unary_overflow_expr (const exprt &expr)
 Cast an exprt to a unary_overflow_exprt. More...
 
unary_overflow_exprtto_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_exprtto_count_leading_zeros_expr (const exprt &expr)
 Cast an exprt to a count_leading_zeros_exprt. More...
 
count_leading_zeros_exprtto_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_exprtto_count_trailing_zeros_expr (const exprt &expr)
 Cast an exprt to a count_trailing_zeros_exprt. More...
 
count_trailing_zeros_exprtto_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_exprtto_bitreverse_expr (const exprt &expr)
 Cast an exprt to a bitreverse_exprt. More...
 
bitreverse_exprtto_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_exprtto_saturating_plus_expr (const exprt &expr)
 Cast an exprt to a saturating_plus_exprt. More...
 
saturating_plus_exprtto_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_exprtto_saturating_minus_expr (const exprt &expr)
 Cast an exprt to a saturating_minus_exprt. More...
 
saturating_minus_exprtto_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_exprtto_overflow_result_expr (const exprt &expr)
 Cast an exprt to a overflow_result_exprt. More...
 
overflow_result_exprtto_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_exprtto_find_first_set_expr (const exprt &expr)
 Cast an exprt to a find_first_set_exprt. More...
 
find_first_set_exprtto_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_exprtto_zero_extend_expr (const exprt &expr)
 Cast an exprt to a zero_extend_exprt. More...
 
zero_extend_exprtto_zero_extend_expr (exprt &expr)
 Cast an exprt to a zero_extend_exprt. More...
 
const onehot_exprtto_onehot_expr (const exprt &expr)
 Cast an exprt to a onehot_exprt. More...
 
onehot_exprtto_onehot_expr (exprt &expr)
 Cast an exprt to a onehot_exprt. More...
 
const onehot0_exprtto_onehot0_expr (const exprt &expr)
 Cast an exprt to a onehot0_exprt. More...
 
onehot0_exprtto_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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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.