cprover
value_sets.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Value Set Propagation
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
13
#define CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
14
15
#include <list>
16
17
#include <
goto-programs/goto_program.h
>
18
19
// an abstract base class
20
21
class
value_setst
22
{
23
public
:
24
value_setst
()
25
{
26
}
27
28
typedef
std::list<exprt>
valuest
;
29
30
// this is not const to allow a lazy evaluation
31
DEPRECATED
(
SINCE
(2019, 05, 22,
"use vector returning version instead"
))
32
virtual
void
get_values
(
33
const
irep_idt
&function_id,
34
goto_programt
::const_targett l,
35
const
exprt
&expr,
36
valuest
&dest) = 0;
37
38
// this is not const to allow a lazy evaluation
39
virtual std::vector<
exprt
>
get_values
(
40
const
irep_idt
&function_id,
41
goto_programt
::const_targett l,
42
const
exprt
&expr) = 0;
43
44
virtual ~
value_setst
()
45
{
46
}
47
};
48
49
#endif // CPROVER_POINTER_ANALYSIS_VALUE_SETS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
exprt
Base class for all expressions.
Definition:
expr.h:53
value_setst::value_setst
value_setst()
Definition:
value_sets.h:24
value_setst::valuest
std::list< exprt > valuest
Definition:
value_sets.h:28
SINCE
#define SINCE(year, month, day, msg)
Definition:
deprecate.h:26
goto_program.h
Concrete Goto Program.
value_setst
Definition:
value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition:
deprecate.h:23
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:73
value_setst::get_values
virtual void get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
pointer-analysis
value_sets.h
Generated by
1.8.20