cprover
bv_cbmc.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_CBMC_BV_CBMC_H
11 #define CPROVER_CBMC_BV_CBMC_H
12 
14 
15 class bv_cbmct:public bv_pointerst
16 {
17 public:
19  const namespacet &_ns,
20  propt &_prop):bv_pointerst(_ns, _prop) { }
21  virtual ~bv_cbmct() { }
22 
23 protected:
24  // overloading
25  virtual bvt convert_bitvector(const exprt &expr); // no cache
26 
27  virtual bvt convert_waitfor(const exprt &expr);
28  virtual bvt convert_waitfor_symbol(const exprt &expr);
29 };
30 
31 #endif // CPROVER_CBMC_BV_CBMC_H
virtual bvt convert_waitfor_symbol(const exprt &expr)
Definition: bv_cbmc.cpp:135
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual bvt convert_bitvector(const exprt &expr)
Definition: bv_cbmc.cpp:158
bv_cbmct(const namespacet &_ns, propt &_prop)
Definition: bv_cbmc.h:18
TO_BE_DOCUMENTED.
Definition: prop.h:22
Base class for all expressions.
Definition: expr.h:46
virtual ~bv_cbmct()
Definition: bv_cbmc.h:21
virtual bvt convert_waitfor(const exprt &expr)
Definition: bv_cbmc.cpp:14
std::vector< literalt > bvt
Definition: literal.h:197