1/*******************************************************************\
3Module: Slicer for symex traces
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
12#ifndef CPROVER_GOTO_SYMEX_SLICE_H
13#define CPROVER_GOTO_SYMEX_SLICE_H
16#include <unordered_set>
23// slice an equation with respect to the assertions contained therein
29// this simply slices away anything after the last assertion
32// Slice the symex trace with respect to a list of given expressions
35 const std::list<exprt> &expressions);
37// Collects "open" variables that are used but not assigned
45#endif // CPROVER_GOTO_SYMEX_SLICE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::unordered_set< irep_idt > symbol_sett
void slice(symex_target_equationt &equation)
void simple_slice(symex_target_equationt &equation)
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
void revert_slice(symex_target_equationt &)
Undo whatever has been done by slice