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 guardt;
20 class exprt;
21 class symbolt;
22 
26 {
27 public:
28  virtual ~dereference_callbackt();
29 
30  virtual void dereference_failure(
31  const std::string &property,
32  const std::string &msg,
33  const guardt &guard)=0;
34 
35  virtual void get_value_set(
36  const exprt &expr,
37  value_setst::valuest &value_set)=0;
38 
39  virtual bool has_failed_symbol(
40  const exprt &expr,
41  const symbolt *&symbol)=0;
42 };
43 
44 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)=0
Definition: guard.h:19
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
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:42
std::list< exprt > valuest
Definition: value_sets.h:28