CBMC
boolbv_update_bits.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
9 #include <util/bitvector_expr.h>
10 
11 #include "boolbv.h"
12 
13 bvt boolbvt::convert_update_bits(const update_bits_exprt &expr)
14 {
15  return convert_bv(expr.lower());
16 }
bitvector_expr.h
API to expression classes for bitvectors.
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:39
boolbvt::convert_update_bits
virtual bvt convert_update_bits(const update_bits_exprt &)
Definition: boolbv_update_bits.cpp:13
update_bits_exprt
Replaces a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:659
update_bits_exprt::lower
exprt lower() const
A lowering to masking, shifting, or.
Definition: bitvector_expr.cpp:79
bvt
std::vector< literalt > bvt
Definition: literal.h:201