CBMC
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 <list>
16 #include <unordered_set>
17 
18 #include <util/irep.h>
19 
20 class exprt;
21 class symex_target_equationt;
22 
23 // slice an equation with respect to the assertions contained therein
24 void slice(symex_target_equationt &equation);
25 
27 void revert_slice(symex_target_equationt &);
28 
29 // this simply slices away anything after the last assertion
30 void simple_slice(symex_target_equationt &equation);
31 
32 // Slice the symex trace with respect to a list of given expressions
33 void slice(
34  symex_target_equationt &equation,
35  const std::list<exprt> &expressions);
36 
37 // Collects "open" variables that are used but not assigned
38 
39 typedef std::unordered_set<irep_idt> symbol_sett;
40 
41 void collect_open_variables(
42  const symex_target_equationt &equation,
43  symbol_sett &open_variables);
44 
45 #endif // CPROVER_GOTO_SYMEX_SLICE_H
revert_slice
void revert_slice(symex_target_equationt &)
Undo whatever has been done by slice
Definition: slice.cpp:261
exprt
Base class for all expressions.
Definition: expr.h:55
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:234
slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:205
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:215
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:33
symbol_sett
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:39
irep.h