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 &equation,
24  const expr_listt &expressions);
25 
27  const symex_target_equationt &equation,
28  symbol_sett &open_variables);
29 
30 protected:
32 
33  void get_symbols(const exprt &expr);
34  void get_symbols(const typet &type);
35 
39 };
40 
41 #endif // CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H
The type of an expression.
Definition: type.h:20
Generate Equation using Symbolic Execution.
symbol_sett depends
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:112
std::unordered_set< irep_idt, irep_id_hash > symbol_sett
Definition: slice.h:29
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
std::list< exprt > expr_listt
Definition: expr.h:166
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:46
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