|
CBMC
|
Include dependency graph for slice.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Typedefs | |
| typedef std::unordered_set< irep_idt > | symbol_sett |
Functions | |
| void | slice (symex_target_equationt &equation) |
| void | revert_slice (symex_target_equationt &) |
Undo whatever has been done by slice More... | |
| void | simple_slice (symex_target_equationt &equation) |
| void | slice (symex_target_equationt &equation, const std::list< exprt > &expressions) |
| Slice the symex trace with respect to a list of expressions. More... | |
| void | collect_open_variables (const symex_target_equationt &equation, symbol_sett &open_variables) |
| Collect the open variables, i.e. More... | |
Slicer for symex traces
Definition in file slice.h.
| typedef std::unordered_set<irep_idt> symbol_sett |
| void collect_open_variables | ( | const symex_target_equationt & | equation, |
| symbol_sett & | open_variables | ||
| ) |
| void revert_slice | ( | symex_target_equationt & | ) |
| void simple_slice | ( | symex_target_equationt & | equation | ) |
| void slice | ( | symex_target_equationt & | equation | ) |
| void slice | ( | symex_target_equationt & | equation, |
| const std::list< exprt > & | expressions | ||
| ) |