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 // slice an equation with respect to the assertions contained therein
18 void slice(symex_target_equationt &equation);
19 
20 // this simply slices away anything after the last assertion
21 void simple_slice(symex_target_equationt &equation);
22 
23 // Slice the symex trace with respect to a list of given expressions
24 void slice(symex_target_equationt &equation,
25  const expr_listt &expressions);
26 
27 // Collects "open" variables that are used but not assigned
28 
29 typedef std::unordered_set<irep_idt, irep_id_hash> symbol_sett;
30 
32  const symex_target_equationt &equation,
33  symbol_sett &open_variables);
34 
35 #endif // CPROVER_GOTO_SYMEX_SLICE_H
Generate Equation using Symbolic Execution.
std::unordered_set< irep_idt, irep_id_hash > symbol_sett
Definition: slice.h:29
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:239
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:220
std::list< exprt > expr_listt
Definition: expr.h:166
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209