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 | bitnor_exprt |
Bit-wise NOR. More... | |
class | bitxor_exprt |
Bit-wise XOR. More... | |
class | bitxnor_exprt |
Bit-wise XNOR. More... | |
class | bitand_exprt |
Bit-wise AND. 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... | |
API to expression classes for bitvectors.
Definition in file bitvector_expr.h.
|
inline |
Definition at line 502 of file bitvector_expr.h.
|
inline |
Definition at line 1066 of file bitvector_expr.h.
|
inline |
Definition at line 309 of file bitvector_expr.h.
|
inline |
Definition at line 353 of file bitvector_expr.h.
|
inline |
Definition at line 183 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 1478 of file bitvector_expr.h.
|
inline |
Definition at line 267 of file bitvector_expr.h.
|
inline |
Definition at line 223 of file bitvector_expr.h.
|
inline |
Definition at line 45 of file bitvector_expr.h.
|
inline |
Definition at line 933 of file bitvector_expr.h.
|
inline |
Definition at line 1334 of file bitvector_expr.h.
|
inline |
Definition at line 1427 of file bitvector_expr.h.
|
inline |
Definition at line 562 of file bitvector_expr.h.
|
inline |
Definition at line 636 of file bitvector_expr.h.
|
inline |
Definition at line 1781 of file bitvector_expr.h.
|
inline |
Definition at line 523 of file bitvector_expr.h.
|
inline |
Definition at line 1138 of file bitvector_expr.h.
|
inline |
Definition at line 1157 of file bitvector_expr.h.
|
inline |
Definition at line 1695 of file bitvector_expr.h.
|
inline |
Definition at line 1119 of file bitvector_expr.h.
|
inline |
Definition at line 977 of file bitvector_expr.h.
|
inline |
Definition at line 877 of file bitvector_expr.h.
|
inline |
Definition at line 1576 of file bitvector_expr.h.
|
inline |
Definition at line 1531 of file bitvector_expr.h.
|
inline |
Definition at line 410 of file bitvector_expr.h.
|
inline |
Definition at line 458 of file bitvector_expr.h.
|
inline |
Definition at line 1172 of file bitvector_expr.h.
|
inline |
Definition at line 1242 of file bitvector_expr.h.
|
inline |
Definition at line 1204 of file bitvector_expr.h.
|
inline |
Definition at line 730 of file bitvector_expr.h.
|
inline |
Definition at line 816 of file bitvector_expr.h.
|
inline |
Definition at line 1833 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 1083 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 1095 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 320 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 327 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnand_exprt.
expr must be known to be bitnand_exprt.
expr | Source expression |
Definition at line 364 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnand_exprt.
expr must be known to be bitnand_exprt.
expr | Source expression |
Definition at line 371 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnor_exprt.
expr must be known to be bitnor_exprt.
expr | Source expression |
Definition at line 194 of file bitvector_expr.h.
|
inline |
Cast an exprt to a bitnor_exprt.
expr must be known to be bitnor_exprt.
expr | Source expression |
Definition at line 201 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 1494 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 1503 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 278 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 286 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 234 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 241 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 944 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 951 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 1351 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 1361 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 1444 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 1454 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 578 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 587 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 652 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 661 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 1797 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 1807 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 1914 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 1922 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 1879 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 1887 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 1720 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 1730 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 993 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 1002 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 893 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 902 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 1592 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 1602 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 1547 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 1557 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 427 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 435 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 469 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 478 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 1259 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 1269 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 741 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 749 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 827 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 835 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 1844 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 1852 of file bitvector_expr.h.
|
inline |
Definition at line 1071 of file bitvector_expr.h.
|
inline |
Definition at line 95 of file bitvector_expr.h.
|
inline |
Definition at line 1483 of file bitvector_expr.h.
|
inline |
Definition at line 50 of file bitvector_expr.h.
|
inline |
Definition at line 1339 of file bitvector_expr.h.
|
inline |
Definition at line 1432 of file bitvector_expr.h.
|
inline |
Definition at line 567 of file bitvector_expr.h.
|
inline |
Definition at line 641 of file bitvector_expr.h.
|
inline |
Definition at line 1786 of file bitvector_expr.h.
|
inline |
Definition at line 1700 of file bitvector_expr.h.
|
inline |
Definition at line 982 of file bitvector_expr.h.
|
inline |
Definition at line 882 of file bitvector_expr.h.
|
inline |
Definition at line 1581 of file bitvector_expr.h.
|
inline |
Definition at line 1536 of file bitvector_expr.h.
|
inline |
Definition at line 416 of file bitvector_expr.h.
|
inline |
Definition at line 1247 of file bitvector_expr.h.
|
inline |
Definition at line 1209 of file bitvector_expr.h.