12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H 40 #endif // CPROVER_GOTO_SYMEX_SYMEX_SLICE_CLASS_H The type of an expression.
Generate Equation using Symbolic Execution.
std::unordered_set< irep_idt > symbol_sett
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
void get_symbols(const exprt &expr)
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...
Base class for all expressions.
void slice(symex_target_equationt &equation)
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)