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:97
TO_BE_DOCUMENTED.
Definition: namespace.h:74
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: bv_cbmc.cpp:109
bv_cbmct(const namespacet &_ns, propt &_prop)
Definition: bv_cbmc.h:18
TO_BE_DOCUMENTED.
Definition: prop.h:24
Base class for all expressions.
Definition: expr.h:42
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:200