25 const std::list<exprt> &exprs)
28 for(
const auto &expr : exprs)
38 for(symex_target_equationt::SSA_stepst::reverse_iterator
144 for(symex_target_equationt::SSA_stepst::const_iterator
153 switch(SSA_step.
type)
202 open_variables.erase(lhs.begin(), lhs.end());
208 symex_slice.
slice(equation);
228 const std::list<exprt> &expressions)
231 symex_slice.
slice(equation, expressions);
237 symex_target_equationt::SSA_stepst::iterator
240 for(symex_target_equationt::SSA_stepst::iterator
249 symex_target_equationt::SSA_stepst::iterator s_it=
Single SSA step in the equation.
goto_trace_stept::typet type
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const irep_idt & id() const
const irep_idt & get_identifier() const
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.
void slice(symex_target_equationt &equation)
void slice_decl(SSA_stept &SSA_step)
void slice_assignment(SSA_stept &SSA_step)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
void slice(symex_target_equationt &equation)
void simple_slice(symex_target_equationt &equation)
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
std::unordered_set< irep_idt > symbol_sett
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.