CBMC
|
Extracts a sub-range of a bit-vector operand. More...
#include <bitvector_expr.h>
Additional Inherited Members | |
![]() | |
typedef std::vector< exprt > | operandst |
![]() | |
using | baset = tree_implementationt |
![]() | |
using | dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true > |
using | subt = typename dt::subt |
using | named_subt = typename dt::named_subt |
using | tree_implementationt = sharing_treet |
Used to refer to this class from derived classes. | |
![]() | |
static void | check (const exprt &, const validation_modet) |
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked). | |
static void | validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness. | |
static void | validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT) |
Check that the expression is well-formed (full check, including checks of all subexpressions and the type) | |
![]() | |
static bool | is_comment (const irep_idt &name) |
static std::size_t | number_of_non_comments (const named_subt &) |
count the number of named_sub elements that are not comments | |
![]() | |
expr_protectedt (irep_idt _id, typet _type) | |
expr_protectedt (irep_idt _id, typet _type, operandst _operands) | |
exprt & | op0 () |
const exprt & | op0 () const |
exprt & | op1 () |
const exprt & | op1 () const |
exprt & | op2 () |
const exprt & | op2 () const |
exprt & | op3 () |
const exprt & | op3 () const |
![]() | |
exprt & | op0 () |
exprt & | op1 () |
exprt & | op2 () |
exprt & | op3 () |
const exprt & | op0 () const |
const exprt & | op1 () const |
const exprt & | op2 () const |
const exprt & | op3 () const |
exprt & | add_expr (const irep_idt &name) |
const exprt & | find_expr (const irep_idt &name) const |
![]() | |
void | detach () |
![]() | |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
Extracts a sub-range of a bit-vector operand.
Definition at line 596 of file bitvector_expr.h.
Extract the bits [_index
.
. _index
+ width - 1] from _src
to produce a result of type _type
where width is the number of bits of _type
. Note that this specifies a closed interval, i.e., both bits _lower
and _index
+ width - 1 are included. Indices count from the least-significant bit, and are not affected by endianness.
Definition at line 604 of file bitvector_expr.h.
Definition at line 31 of file bitvector_expr.cpp.
|
inline |
Definition at line 619 of file bitvector_expr.h.
Definition at line 629 of file bitvector_expr.h.
|
inline |
Definition at line 614 of file bitvector_expr.h.
Definition at line 624 of file bitvector_expr.h.