CBMC
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 
27 class dereference_callbackt
28 {
29 public:
30  virtual ~dereference_callbackt() = default;
31 
32  virtual std::vector<exprt> get_value_set(const exprt &expr) const = 0;
33 
34  virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
35 };
36 
37 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:27
exprt
Base class for all expressions.
Definition: expr.h:55
dereference_callbackt::get_or_create_failed_symbol
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
dereference_callbackt::get_value_set
virtual std::vector< exprt > get_value_set(const exprt &expr) const =0
value_sets.h
symbolt
Symbol table entry.
Definition: symbol.h:27
dereference_callbackt::~dereference_callbackt
virtual ~dereference_callbackt()=default