cprover
bv_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
11 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
12 
13 
14 #include "boolbv.h"
15 #include "pointer_logic.h"
16 
17 class bv_pointerst:public boolbvt
18 {
19 public:
20  bv_pointerst(const namespacet &_ns, propt &_prop);
21 
22  void post_process() override;
23 
24 protected:
26 
27  // NOLINTNEXTLINE(readability/identifiers)
28  typedef boolbvt SUB;
29 
31 
32  void encode(std::size_t object, bvt &bv);
33 
34  virtual bvt convert_pointer_type(const exprt &expr);
35 
36  virtual void add_addr(const exprt &expr, bvt &bv);
37 
38  // overloading
39  literalt convert_rest(const exprt &expr) override;
40  bvt convert_bitvector(const exprt &expr) override; // no cache
41 
43  const bvt &bv,
44  const std::vector<bool> &unknown,
45  std::size_t offset,
46  const typet &type) const override;
47 
49  const exprt &expr,
50  bvt &bv);
51 
52  void offset_arithmetic(bvt &bv, const mp_integer &x);
53  void offset_arithmetic(bvt &bv, const mp_integer &factor, const exprt &index);
54  void offset_arithmetic(
55  bvt &bv, const mp_integer &factor, const bvt &index_bv);
56 
57  struct postponedt
58  {
59  bvt bv, op;
61  };
62 
63  typedef std::list<postponedt> postponed_listt;
65 
66  void do_postponed(const postponedt &postponed);
67 };
68 
69 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
bv_pointerst::object_bits
unsigned object_bits
Definition: bv_pointers.h:30
bv_pointerst::convert_address_of_rec
bool convert_address_of_rec(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:94
bv_pointerst::postponedt::op
bvt op
Definition: bv_pointers.h:59
typet
The type of an expression, extends irept.
Definition: type.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
bv_pointerst::postponed_list
postponed_listt postponed_list
Definition: bv_pointers.h:64
bv_pointerst::postponedt::expr
exprt expr
Definition: bv_pointers.h:60
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
bv_pointerst::bv_get_rec
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Definition: bv_pointers.cpp:596
bv_pointerst::do_postponed
void do_postponed(const postponedt &postponed)
Definition: bv_pointers.cpp:737
exprt
Base class for all expressions.
Definition: expr.h:54
pointer_logict
Definition: pointer_logic.h:22
bv_pointerst::convert_pointer_type
virtual bvt convert_pointer_type(const exprt &expr)
Definition: bv_pointers.cpp:219
bv_pointerst::postponed_listt
std::list< postponedt > postponed_listt
Definition: bv_pointers.h:63
bv_pointerst::SUB
boolbvt SUB
Definition: bv_pointers.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
pointer_logic.h
bv_pointerst::convert_bitvector
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: bv_pointers.cpp:471
bv_pointerst::pointer_logic
pointer_logict pointer_logic
Definition: bv_pointers.h:25
bv_pointerst
Definition: bv_pointers.h:17
bv_pointerst::bits
unsigned bits
Definition: bv_pointers.h:30
bv_pointerst::encode
void encode(std::size_t object, bvt &bv)
Definition: bv_pointers.cpp:654
bv_pointerst::offset_bits
unsigned offset_bits
Definition: bv_pointers.h:30
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
bv_pointerst::postponedt
Definition: bv_pointers.h:57
literalt
Definition: literal.h:24
boolbvt
Definition: boolbv.h:32
bv_pointerst::bv_pointerst
bv_pointerst(const namespacet &_ns, propt &_prop)
Definition: bv_pointers.cpp:82
boolbv.h
bv_pointerst::offset_arithmetic
void offset_arithmetic(bvt &bv, const mp_integer &x)
Definition: bv_pointers.cpp:667
bv_pointerst::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:17
bv_pointerst::post_process
void post_process() override
Definition: bv_pointers.cpp:827
bv_pointerst::add_addr
virtual void add_addr(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:721
bv_pointerst::postponedt::bv
bvt bv
Definition: bv_pointers.h:59