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
27
class
dereference_callbackt
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
dereference_callbackt
Base class for pointer value set analysis.
Definition:
dereference_callback.h:27
dereference_callbackt::get_value_set
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
exprt
Base class for all expressions.
Definition:
expr.h:54
value_sets.h
value_setst::valuest
std::list< exprt > valuest
Definition:
value_sets.h:28
dereference_callbackt::has_failed_symbol
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
symbolt
Symbol table entry.
Definition:
symbol.h:27
dereference_callbackt::~dereference_callbackt
virtual ~dereference_callbackt()=default
pointer-analysis
dereference_callback.h
Generated by
1.8.17