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  virtual void get_value_set(
33  const exprt &expr,
34  value_setst::valuest &value_set)=0;
35 
36  virtual bool has_failed_symbol(
37  const exprt &expr,
38  const symbolt *&symbol)=0;
39 };
40 
41 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
Base class for pointer value set analysis.
Symbol table entry.
Definition: symbol.h:27
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
virtual ~dereference_callbackt()=default
Value Set Propagation.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
Base class for all expressions.
Definition: expr.h:54
std::list< exprt > valuest
Definition: value_sets.h:28