cprover
dereference_callback.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Dereferencing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
13 #define CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
14 
15 #include <string>
16 
17 #include "value_sets.h"
18 
19 class exprt;
20 class symbolt;
21 
28 {
29 public:
30  virtual ~dereference_callbackt() = default;
31 
32  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
33  virtual void
34  get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
35 
36  virtual std::vector<exprt> get_value_set(const exprt &expr) const = 0;
37 
38  virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
39 };
40 
41 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
dereference_callbackt::get_value_set
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set) const =0
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:28
exprt
Base class for all expressions.
Definition: expr.h:53
dereference_callbackt::get_or_create_failed_symbol
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
value_sets.h
Value Set Propagation.
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
value_setst
Definition: value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
dereference_callbackt::~dereference_callbackt
virtual ~dereference_callbackt()=default