cprover
slice.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Slicer for symex traces
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_SYMEX_SLICE_H
13
#define CPROVER_GOTO_SYMEX_SLICE_H
14
15
#include "
symex_target_equation.h
"
16
17
#include <list>
18
19
// slice an equation with respect to the assertions contained therein
20
void
slice
(
symex_target_equationt
&equation);
21
23
void
revert_slice
(
symex_target_equationt
&);
24
25
// this simply slices away anything after the last assertion
26
void
simple_slice
(
symex_target_equationt
&equation);
27
28
// Slice the symex trace with respect to a list of given expressions
29
void
slice
(
30
symex_target_equationt
&equation,
31
const
std::list<exprt> &expressions);
32
33
// Collects "open" variables that are used but not assigned
34
35
typedef
std::unordered_set<irep_idt>
symbol_sett
;
36
37
void
collect_open_variables
(
38
const
symex_target_equationt
&equation,
39
symbol_sett
&open_variables);
40
41
#endif // CPROVER_GOTO_SYMEX_SLICE_H
revert_slice
void revert_slice(symex_target_equationt &)
Undo whatever has been done by slice
Definition:
slice.cpp:264
symex_target_equation.h
Generate Equation using Symbolic Execution.
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition:
slice.cpp:237
slice
void slice(symex_target_equationt &equation)
Definition:
slice.cpp:206
collect_open_variables
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition:
slice.cpp:217
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition:
symex_target_equation.h:41
symbol_sett
std::unordered_set< irep_idt > symbol_sett
Definition:
slice.h:35
goto-symex
slice.h
Generated by
1.8.20