25 if(expr.
id()==ID_symbol)
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);
236 symex_slice.
slice(equation, expressions);
242 symex_target_equationt::SSA_stepst::iterator
245 for(symex_target_equationt::SSA_stepst::iterator
254 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
const irep_idt & id() const
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
std::unordered_set< irep_idt, irep_id_hash > symbol_sett
void get_symbols(const exprt &expr)
API to expression classes.
#define forall_operands(it, expr)
std::list< exprt > expr_listt
#define forall_expr_list(it, 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.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
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