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
DEPRECATED
(
SINCE
(2019, 05, 22,
"use vector returning version instead"
))
33
virtual
void
34
get_value_set
(const
exprt
&expr,
value_setst
::valuest &value_set) const = 0;
35
36
virtual std::vector<
exprt
>
get_value_set
(const
exprt
&expr) const = 0;
37
38
virtual const
symbolt
*
get_or_create_failed_symbol
(const
exprt
&expr) = 0;
39
};
40
41
#endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H
dereference_callbackt::get_value_set
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set) const =0
dereference_callbackt
Base class for pointer value set analysis.
Definition:
dereference_callback.h:28
exprt
Base class for all expressions.
Definition:
expr.h:53
dereference_callbackt::get_or_create_failed_symbol
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
value_sets.h
Value Set Propagation.
SINCE
#define SINCE(year, month, day, msg)
Definition:
deprecate.h:26
value_setst
Definition:
value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition:
deprecate.h:23
symbolt
Symbol table entry.
Definition:
symbol.h:28
dereference_callbackt::~dereference_callbackt
virtual ~dereference_callbackt()=default
pointer-analysis
dereference_callback.h
Generated by
1.8.20