CBMC
|
Slicer for symex traces. More...
#include "slice.h"
#include "symex_slice_class.h"
#include <util/find_symbols.h>
#include <util/std_expr.h>
Go to the source code of this file.
Functions | |
void | slice (symex_target_equationt &equation) |
void | collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables) |
Collect the open variables, i.e. More... | |
void | slice (symex_target_equationt &equation, const std::list< exprt > &expressions) |
Slice the symex trace with respect to a list of expressions. More... | |
void | simple_slice (symex_target_equationt &equation) |
void | revert_slice (symex_target_equationt &equation) |
Undo whatever has been done by slice More... | |
Slicer for symex traces.
Definition in file slice.cpp.
void collect_open_variables | ( | const symex_target_equationt & | equation, |
symbol_sett & | open_variables | ||
) |
void revert_slice | ( | symex_target_equationt & | equation | ) |
void simple_slice | ( | symex_target_equationt & | equation | ) |
void slice | ( | symex_target_equationt & | equation | ) |
void slice | ( | symex_target_equationt & | equation, |
const std::list< exprt > & | expressions | ||
) |