cprover
|
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 | 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 | unary_overflow_exprt |
A Boolean expression returning true, iff operation kind 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... | |
API to expression classes for bitvectors.
Definition in file bitvector_expr.h.
|
inline |
Definition at line 723 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 169 of file bitvector_expr.h.
|
inline |
Definition at line 45 of file bitvector_expr.h.
|
inline |
Definition at line 607 of file bitvector_expr.h.
|
inline |
Definition at line 882 of file bitvector_expr.h.
|
inline |
Definition at line 395 of file bitvector_expr.h.
|
inline |
Definition at line 483 of file bitvector_expr.h.
|
inline |
Definition at line 651 of file bitvector_expr.h.
|
inline |
Definition at line 551 of file bitvector_expr.h.
|
inline |
Definition at line 261 of file bitvector_expr.h.
|
inline |
Definition at line 790 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 741 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 753 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 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 618 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 625 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 899 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 909 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 411 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 420 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 499 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 508 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 667 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 676 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 567 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 576 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 314 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 323 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 807 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 817 of file bitvector_expr.h.
|
inline |
Definition at line 729 of file bitvector_expr.h.
|
inline |
Definition at line 95 of file bitvector_expr.h.
|
inline |
Definition at line 50 of file bitvector_expr.h.
|
inline |
Definition at line 887 of file bitvector_expr.h.
|
inline |
Definition at line 400 of file bitvector_expr.h.
|
inline |
Definition at line 488 of file bitvector_expr.h.
|
inline |
Definition at line 656 of file bitvector_expr.h.
|
inline |
Definition at line 556 of file bitvector_expr.h.
|
inline |
Definition at line 267 of file bitvector_expr.h.
|
inline |
Definition at line 795 of file bitvector_expr.h.