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, extends irept.
Generate Equation using Symbolic Execution.
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_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...
Single SSA step in the equation.
Base class for all expressions.
void slice(symex_target_equationt &equation)
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)