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;
64  postponed_listt postponed_list;
65 
66  void do_postponed(const postponedt &postponed);
67 
68  static bool is_ptr(const typet &type)
69  {
70  return type.id()==ID_pointer || type.id()==ID_reference;
71  }
72 };
73 
74 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
The type of an expression.
Definition: type.h:20
boolbvt SUB
Definition: bv_pointers.h:28
BigInt mp_integer
Definition: mp_arith.h:19
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:19
bvt convert_bitvector(const exprt &expr) override
static bool is_ptr(const typet &type)
Definition: bv_pointers.h:68
Definition: boolbv.h:31
std::list< postponedt > postponed_listt
Definition: bv_pointers.h:63
const irep_idt & id() const
Definition: irep.h:189
unsigned offset_bits
Definition: bv_pointers.h:30
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
Definition: bv_pointers.h:25
unsigned object_bits
Definition: bv_pointers.h:30
TO_BE_DOCUMENTED.
Definition: namespace.h:62
TO_BE_DOCUMENTED.
Definition: prop.h:22
bv_pointerst(const namespacet &_ns, propt &_prop)
Definition: bv_pointers.cpp:92
postponed_listt postponed_list
Definition: bv_pointers.h:64
void post_process() override
void encode(std::size_t object, bvt &bv)
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Base class for all expressions.
Definition: expr.h:46
void do_postponed(const postponedt &postponed)
virtual bvt convert_pointer_type(const exprt &expr)
bool convert_address_of_rec(const exprt &expr, bvt &bv)
unsigned bits
Definition: bv_pointers.h:30
Pointer Logic.
std::vector< literalt > bvt
Definition: literal.h:197
void offset_arithmetic(bvt &bv, const mp_integer &x)