CBMC
value_sets.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
14 
15 #include <list>
16 
18 
19 // an abstract base class
20 
22 {
23 public:
25  {
26  }
27 
28  typedef std::list<exprt> valuest;
29 
30  // this is not const to allow a lazy evaluation
31  virtual std::vector<exprt> get_values(
32  const irep_idt &function_id,
34  const exprt &expr) = 0;
35 
36  virtual ~value_setst()
37  {
38  }
39 };
40 
41 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
instructionst::const_iterator const_targett
Definition: goto_program.h:615
std::list< exprt > valuest
Definition: value_sets.h:28
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
virtual ~value_setst()
Definition: value_sets.h:36
Concrete Goto Program.