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:
21  const namespacet &_ns,
22  propt &_prop,
23  message_handlert &message_handler);
24 
25  void post_process() override;
26 
27 protected:
29 
30  // NOLINTNEXTLINE(readability/identifiers)
31  typedef boolbvt SUB;
32 
34 
35  void encode(std::size_t object, bvt &bv);
36 
37  virtual bvt convert_pointer_type(const exprt &expr);
38 
39  virtual void add_addr(const exprt &expr, bvt &bv);
40 
41  // overloading
42  literalt convert_rest(const exprt &expr) override;
43  bvt convert_bitvector(const exprt &expr) override; // no cache
44 
46  const exprt &expr,
47  const bvt &bv,
48  const std::vector<bool> &unknown,
49  std::size_t offset,
50  const typet &type) const override;
51 
53  const exprt &expr,
54  bvt &bv);
55 
56  void offset_arithmetic(bvt &bv, const mp_integer &x);
57  void offset_arithmetic(bvt &bv, const mp_integer &factor, const exprt &index);
58  void offset_arithmetic(
59  bvt &bv, const mp_integer &factor, const bvt &index_bv);
60 
61  struct postponedt
62  {
63  bvt bv, op;
65  };
66 
67  typedef std::list<postponedt> postponed_listt;
69 
70  void do_postponed(const postponedt &postponed);
71 };
72 
73 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
bv_pointerst::object_bits
unsigned object_bits
Definition: bv_pointers.h:33
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:63
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_pointerst::postponed_list
postponed_listt postponed_list
Definition: bv_pointers.h:68
bv_pointerst::postponedt::expr
exprt expr
Definition: bv_pointers.h:64
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
bv_pointerst::bv_pointerst
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
Definition: bv_pointers.cpp:82
bv_pointerst::do_postponed
void do_postponed(const postponedt &postponed)
Definition: bv_pointers.cpp:736
exprt
Base class for all expressions.
Definition: expr.h:53
bv_pointerst::bv_get_rec
exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Definition: bv_pointers.cpp:594
pointer_logict
Definition: pointer_logic.h:23
bv_pointerst::convert_pointer_type
virtual bvt convert_pointer_type(const exprt &expr)
Definition: bv_pointers.cpp:218
bv_pointerst::postponed_listt
std::list< postponedt > postponed_listt
Definition: bv_pointers.h:67
bv_pointerst::SUB
boolbvt SUB
Definition: bv_pointers.h:31
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
pointer_logic.h
Pointer Logic.
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:28
bv_pointerst
Definition: bv_pointers.h:18
bv_pointerst::bits
unsigned bits
Definition: bv_pointers.h:33
message_handlert
Definition: message.h:28
bv_pointerst::encode
void encode(std::size_t object, bvt &bv)
Definition: bv_pointers.cpp:653
bv_pointerst::offset_bits
unsigned offset_bits
Definition: bv_pointers.h:33
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
bv_pointerst::postponedt
Definition: bv_pointers.h:62
literalt
Definition: literal.h:26
boolbvt
Definition: boolbv.h:35
boolbv.h
bv_pointerst::offset_arithmetic
void offset_arithmetic(bvt &bv, const mp_integer &x)
Definition: bv_pointers.cpp:666
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:816
bv_pointerst::add_addr
virtual void add_addr(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:720
bv_pointerst::postponedt::bv
bvt bv
Definition: bv_pointers.h:63