cprover
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  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
32  virtual void get_values(
33  const irep_idt &function_id,
34  goto_programt::const_targett l,
35  const exprt &expr,
36  valuest &dest) = 0;
37 
38  // this is not const to allow a lazy evaluation
39  virtual std::vector<exprt> get_values(
40  const irep_idt &function_id,
41  goto_programt::const_targett l,
42  const exprt &expr) = 0;
43 
44  virtual ~value_setst()
45  {
46  }
47 };
48 
49 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
exprt
Base class for all expressions.
Definition: expr.h:53
value_setst::value_setst
value_setst()
Definition: value_sets.h:24
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
goto_program.h
Concrete Goto Program.
value_setst
Definition: value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
value_setst::get_values
virtual void get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr, valuest &dest)=0