CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dereference_callback.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Dereferencing
4
5Author: 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
19class exprt;
20class symbolt;
21
28{
29public:
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
Base class for pointer value set analysis.
virtual ~dereference_callbackt()=default
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
virtual std::vector< exprt > get_value_set(const exprt &expr) const =0
Base class for all expressions.
Definition expr.h:56
Symbol table entry.
Definition symbol.h:28
Value Set Propagation.