cprover
Loading...
Searching...
No Matches
symex_slice_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicer for symex traces
4
5Author: 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
16#include "slice.h"
17
19{
20public:
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
29protected:
31
32 void get_symbols(const exprt &expr);
33 void get_symbols(const typet &type);
34
35 void slice(SSA_stept &SSA_step);
36 void slice_assignment(SSA_stept &SSA_step);
37 void slice_decl(SSA_stept &SSA_step);
38};
39
40#endif // CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H
Single SSA step in the equation.
Definition: ssa_step.h:47
Base class for all expressions.
Definition: expr.h:54
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:141
symbol_sett depends
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
void slice_decl(SSA_stept &SSA_step)
Definition: slice.cpp:126
void slice_assignment(SSA_stept &SSA_step)
Definition: slice.cpp:112
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The type of an expression, extends irept.
Definition: type.h:29
Slicer for symex traces.
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:39
Generate Equation using Symbolic Execution.