slice.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Slicer for symex traces
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SLICE_H
#define CPROVER_GOTO_SYMEX_SLICE_H
 
#include <list>
#include <unordered_set>
 
#include <util/irep.h>
 
class exprt;
class symex_target_equationt;
 
// slice an equation with respect to the assertions contained therein
void slice(symex_target_equationt &equation);
 
void revert_slice(symex_target_equationt &);
 
// this simply slices away anything after the last assertion
void simple_slice(symex_target_equationt &equation);
 
// Slice the symex trace with respect to a list of given expressions
void slice(
  symex_target_equationt &equation,
  const std::list<exprt> &expressions);
 
// Collects "open" variables that are used but not assigned
 
typedef std::unordered_set<irep_idt> symbol_sett;
 
void collect_open_variables(
  const symex_target_equationt &equation,
  symbol_sett &open_variables);
 
#endif // CPROVER_GOTO_SYMEX_SLICE_H