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 | 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... | |
API to expression classes for bitvectors.
Definition in file bitvector_expr.h.
|
inline |
Definition at line 353 of file bitvector_expr.h.
|
inline |
Definition at line 917 of file bitvector_expr.h.
|
inline |
Definition at line 204 of file bitvector_expr.h.
|
inline |
Definition at line 90 of file bitvector_expr.h.
|
inline |
Definition at line 134 of file bitvector_expr.h.
|
inline |
Definition at line 1329 of file bitvector_expr.h.
|
inline |
Definition at line 169 of file bitvector_expr.h.
|
inline |
Definition at line 45 of file bitvector_expr.h.
|
inline |
Definition at line 784 of file bitvector_expr.h.
|
inline |
Definition at line 1185 of file bitvector_expr.h.
|
inline |
Definition at line 1278 of file bitvector_expr.h.
|
inline |
Definition at line 413 of file bitvector_expr.h.
|
inline |
Definition at line 487 of file bitvector_expr.h.
|
inline |
Definition at line 1632 of file bitvector_expr.h.
|
inline |
Definition at line 374 of file bitvector_expr.h.
|
inline |
Definition at line 989 of file bitvector_expr.h.
|
inline |
Definition at line 1008 of file bitvector_expr.h.
|
inline |
Definition at line 1546 of file bitvector_expr.h.
|
inline |
Definition at line 970 of file bitvector_expr.h.
|
inline |
Definition at line 828 of file bitvector_expr.h.
|
inline |
Definition at line 728 of file bitvector_expr.h.
|
inline |
Definition at line 1427 of file bitvector_expr.h.
|
inline |
Definition at line 1382 of file bitvector_expr.h.
|
inline |
Definition at line 261 of file bitvector_expr.h.
|
inline |
Definition at line 309 of file bitvector_expr.h.
|
inline |
Definition at line 1023 of file bitvector_expr.h.
|
inline |
Definition at line 1093 of file bitvector_expr.h.
|
inline |
Definition at line 1055 of file bitvector_expr.h.
|
inline |
Definition at line 581 of file bitvector_expr.h.
|
inline |
Definition at line 667 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 934 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 946 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 215 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 222 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 145 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 152 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 1345 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 1354 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 180 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 187 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 795 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 802 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 1202 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 1212 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 1295 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 1305 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 429 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 438 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 503 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 512 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 1648 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 1658 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 1571 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 1581 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 844 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 853 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 744 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 753 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 1443 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 1453 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 1398 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 1408 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 278 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 286 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 320 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 329 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 1110 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 1120 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 592 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 600 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 678 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 686 of file bitvector_expr.h.
|
inline |
Definition at line 922 of file bitvector_expr.h.
|
inline |
Definition at line 95 of file bitvector_expr.h.
|
inline |
Definition at line 1334 of file bitvector_expr.h.
|
inline |
Definition at line 50 of file bitvector_expr.h.
|
inline |
Definition at line 1190 of file bitvector_expr.h.
|
inline |
Definition at line 1283 of file bitvector_expr.h.
|
inline |
Definition at line 418 of file bitvector_expr.h.
|
inline |
Definition at line 492 of file bitvector_expr.h.
|
inline |
Definition at line 1637 of file bitvector_expr.h.
|
inline |
Definition at line 1551 of file bitvector_expr.h.
|
inline |
Definition at line 833 of file bitvector_expr.h.
|
inline |
Definition at line 733 of file bitvector_expr.h.
|
inline |
Definition at line 1432 of file bitvector_expr.h.
|
inline |
Definition at line 1387 of file bitvector_expr.h.
|
inline |
Definition at line 267 of file bitvector_expr.h.
|
inline |
Definition at line 1098 of file bitvector_expr.h.
|
inline |
Definition at line 1060 of file bitvector_expr.h.