cprover
symex_slice_class.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_SYMEX_SLICE_CLASS_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H
14 
15 #include "symex_target_equation.h"
16 #include "slice.h"
17 
19 {
20 public:
21  void slice(symex_target_equationt &equation);
22 
23  void slice(symex_target_equationt &, const std::list<exprt> &);
24 
26  const symex_target_equationt &equation,
27  symbol_sett &open_variables);
28 
29 protected:
31 
32  void get_symbols(const exprt &expr);
33  void get_symbols(const typet &type);
34 
38 };
39 
40 #endif // CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H
The type of an expression.
Definition: type.h:22
Generate Equation using Symbolic Execution.
symbol_sett depends
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:32
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:112
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e., variables that are used in RHS but never written in LHS...
Definition: slice.cpp:145
Base class for all expressions.
Definition: expr.h:42
Slicer for symex traces.
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:127