25 if(expr.
id()==ID_symbol)
36 const std::list<exprt> &exprs)
39 for(
const auto &expr : exprs)
47 for(symex_target_equationt::SSA_stepst::reverse_iterator
115 assert(SSA_step.
ssa_lhs.
id()==ID_symbol);
130 assert(SSA_step.
ssa_lhs.
id()==ID_symbol);
151 for(symex_target_equationt::SSA_stepst::const_iterator
160 switch(SSA_step.
type)
206 open_variables.erase(lhs.begin(), lhs.end());
212 symex_slice.
slice(equation);
234 const std::list<exprt> &expressions)
237 symex_slice.
slice(equation, expressions);
243 symex_target_equationt::SSA_stepst::iterator
246 for(symex_target_equationt::SSA_stepst::iterator
255 symex_target_equationt::SSA_stepst::iterator s_it=
The type of an expression.
void slice(symex_target_equationt &equation)
void simple_slice(symex_target_equationt &equation)
const irep_idt & get_identifier() const
std::unordered_set< irep_idt > symbol_sett
const irep_idt & id() const
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
void get_symbols(const exprt &expr)
API to expression classes.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
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 collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)
goto_trace_stept::typet type