CBMC
|
API to expression classes for bitvectors. More...
#include "std_expr.h"
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... | |
API to expression classes for bitvectors.
Definition in file bitvector_expr.h.
|
inline |
Definition at line 403 of file bitvector_expr.h.
|
inline |
Definition at line 967 of file bitvector_expr.h.
|
inline |
Definition at line 254 of file bitvector_expr.h.
|
inline |
Definition at line 90 of file bitvector_expr.h.
|
inline |
Definition at line 139 of file bitvector_expr.h.
|
inline |
Definition at line 1379 of file bitvector_expr.h.
|
inline |
Definition at line 214 of file bitvector_expr.h.
|
inline |
Definition at line 179 of file bitvector_expr.h.
|
inline |
Definition at line 45 of file bitvector_expr.h.
|
inline |
Definition at line 834 of file bitvector_expr.h.
|
inline |
Definition at line 1235 of file bitvector_expr.h.
|
inline |
Definition at line 1328 of file bitvector_expr.h.
|
inline |
Definition at line 463 of file bitvector_expr.h.
|
inline |
Definition at line 537 of file bitvector_expr.h.
|
inline |
Definition at line 1682 of file bitvector_expr.h.
|
inline |
Definition at line 424 of file bitvector_expr.h.
|
inline |
Definition at line 1039 of file bitvector_expr.h.
|
inline |
Definition at line 1058 of file bitvector_expr.h.
|
inline |
Definition at line 1596 of file bitvector_expr.h.
|
inline |
Definition at line 1020 of file bitvector_expr.h.
|
inline |
Definition at line 878 of file bitvector_expr.h.
|
inline |
Definition at line 778 of file bitvector_expr.h.
|
inline |
Definition at line 1477 of file bitvector_expr.h.
|
inline |
Definition at line 1432 of file bitvector_expr.h.
|
inline |
Definition at line 311 of file bitvector_expr.h.
|
inline |
Definition at line 359 of file bitvector_expr.h.
|
inline |
Definition at line 1073 of file bitvector_expr.h.
|
inline |
Definition at line 1143 of file bitvector_expr.h.
|
inline |
Definition at line 1105 of file bitvector_expr.h.
|
inline |
Definition at line 631 of file bitvector_expr.h.
|
inline |
Definition at line 717 of file bitvector_expr.h.
|
inline |
Definition at line 1734 of file bitvector_expr.h.
|
inline |
Cast an exprt to a binary_overflow_exprt.
expr must be known to be binary_overflow_exprt.
expr | Source expression |
Definition at line 984 of file bitvector_expr.h.
|
inline |
Cast an exprt to a binary_overflow_exprt.
expr must be known to be binary_overflow_exprt.
expr | Source expression |
Definition at line 996 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 265 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 272 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 106 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 115 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 150 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 157 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitreverse_exprt.
expr must be known to be bitreverse_exprt.
expr | Source expression |
Definition at line 1395 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitreverse_exprt.
expr must be known to be bitreverse_exprt.
expr | Source expression |
Definition at line 1404 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitxnor_exprt.
expr must be known to be bitxnor_exprt.
expr | Source expression |
Definition at line 225 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitxnor_exprt.
expr must be known to be bitxnor_exprt.
expr | Source expression |
Definition at line 232 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 190 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 197 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 63 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 72 of file bitvector_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 845 of file bitvector_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 852 of file bitvector_expr.h.
|
inline |
Cast an exprt to a count_leading_zeros_exprt.
expr must be known to be count_leading_zeros_exprt.
expr | Source expression |
Definition at line 1252 of file bitvector_expr.h.
|
inline |
Cast an exprt to a count_leading_zeros_exprt.
expr must be known to be count_leading_zeros_exprt.
expr | Source expression |
Definition at line 1262 of file bitvector_expr.h.
|
inline |
Cast an exprt to a count_trailing_zeros_exprt.
expr must be known to be count_trailing_zeros_exprt.
expr | Source expression |
Definition at line 1345 of file bitvector_expr.h.
|
inline |
Cast an exprt to a count_trailing_zeros_exprt.
expr must be known to be count_trailing_zeros_exprt.
expr | Source expression |
Definition at line 1355 of file bitvector_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 479 of file bitvector_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 488 of file bitvector_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 553 of file bitvector_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 562 of file bitvector_expr.h.
|
inline |
Cast an exprt to a find_first_set_exprt.
expr must be known to be find_first_set_exprt.
expr | Source expression |
Definition at line 1698 of file bitvector_expr.h.
|
inline |
Cast an exprt to a find_first_set_exprt.
expr must be known to be find_first_set_exprt.
expr | Source expression |
Definition at line 1708 of file bitvector_expr.h.
|
inline |
Cast an exprt to a onehot0_exprt.
expr must be known to be onehot0_exprt.
expr | Source expression |
Definition at line 1815 of file bitvector_expr.h.
|
inline |
Cast an exprt to a onehot0_exprt.
expr must be known to be onehot0_exprt.
expr | Source expression |
Definition at line 1823 of file bitvector_expr.h.
|
inline |
Cast an exprt to a onehot_exprt.
expr must be known to be onehot_exprt.
expr | Source expression |
Definition at line 1780 of file bitvector_expr.h.
|
inline |
Cast an exprt to a onehot_exprt.
expr must be known to be onehot_exprt.
expr | Source expression |
Definition at line 1788 of file bitvector_expr.h.
|
inline |
Cast an exprt to a overflow_result_exprt.
expr must be known to be overflow_result_exprt.
expr | Source expression |
Definition at line 1621 of file bitvector_expr.h.
|
inline |
Cast an exprt to a overflow_result_exprt.
expr must be known to be overflow_result_exprt.
expr | Source expression |
Definition at line 1631 of file bitvector_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 894 of file bitvector_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 903 of file bitvector_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 794 of file bitvector_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 803 of file bitvector_expr.h.
|
inline |
Cast an exprt to a saturating_minus_exprt.
expr must be known to be saturating_minus_exprt.
expr | Source expression |
Definition at line 1493 of file bitvector_expr.h.
|
inline |
Cast an exprt to a saturating_minus_exprt.
expr must be known to be saturating_minus_exprt.
expr | Source expression |
Definition at line 1503 of file bitvector_expr.h.
|
inline |
Cast an exprt to a saturating_plus_exprt.
expr must be known to be saturating_plus_exprt.
expr | Source expression |
Definition at line 1448 of file bitvector_expr.h.
|
inline |
Cast an exprt to a saturating_plus_exprt.
expr must be known to be saturating_plus_exprt.
expr | Source expression |
Definition at line 1458 of file bitvector_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 328 of file bitvector_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 336 of file bitvector_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 370 of file bitvector_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 379 of file bitvector_expr.h.
|
inline |
Cast an exprt to a unary_overflow_exprt.
expr must be known to be unary_overflow_exprt.
expr | Source expression |
Definition at line 1160 of file bitvector_expr.h.
|
inline |
Cast an exprt to a unary_overflow_exprt.
expr must be known to be unary_overflow_exprt.
expr | Source expression |
Definition at line 1170 of file bitvector_expr.h.
|
inline |
Cast an exprt to an update_bit_exprt.
expr must be known to be update_bit_exprt.
expr | Source expression |
Definition at line 642 of file bitvector_expr.h.
|
inline |
Cast an exprt to an update_bit_exprt.
expr must be known to be update_bit_exprt.
expr | Source expression |
Definition at line 650 of file bitvector_expr.h.
|
inline |
Cast an exprt to an update_bits_exprt.
expr must be known to be update_bits_exprt.
expr | Source expression |
Definition at line 728 of file bitvector_expr.h.
|
inline |
Cast an exprt to an update_bits_exprt.
expr must be known to be update_bits_exprt.
expr | Source expression |
Definition at line 736 of file bitvector_expr.h.
|
inline |
Cast an exprt to a zero_extend_exprt.
expr must be known to be zero_extend_exprt.
expr | Source expression |
Definition at line 1745 of file bitvector_expr.h.
|
inline |
Cast an exprt to a zero_extend_exprt.
expr must be known to be zero_extend_exprt.
expr | Source expression |
Definition at line 1753 of file bitvector_expr.h.
|
inline |
Definition at line 972 of file bitvector_expr.h.
|
inline |
Definition at line 95 of file bitvector_expr.h.
|
inline |
Definition at line 1384 of file bitvector_expr.h.
|
inline |
Definition at line 50 of file bitvector_expr.h.
|
inline |
Definition at line 1240 of file bitvector_expr.h.
|
inline |
Definition at line 1333 of file bitvector_expr.h.
|
inline |
Definition at line 468 of file bitvector_expr.h.
|
inline |
Definition at line 542 of file bitvector_expr.h.
|
inline |
Definition at line 1687 of file bitvector_expr.h.
|
inline |
Definition at line 1601 of file bitvector_expr.h.
|
inline |
Definition at line 883 of file bitvector_expr.h.
|
inline |
Definition at line 783 of file bitvector_expr.h.
|
inline |
Definition at line 1482 of file bitvector_expr.h.
|
inline |
Definition at line 1437 of file bitvector_expr.h.
|
inline |
Definition at line 317 of file bitvector_expr.h.
|
inline |
Definition at line 1148 of file bitvector_expr.h.
|
inline |
Definition at line 1110 of file bitvector_expr.h.