Go to the documentation of this file.
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
148 for(symex_target_equationt::SSA_stepst::const_iterator
157 switch(SSA_step.
type)
203 open_variables.erase(lhs.begin(), lhs.end());
209 symex_slice.
slice(equation);
231 const std::list<exprt> &expressions)
234 symex_slice.
slice(equation, expressions);
240 symex_target_equationt::SSA_stepst::iterator
243 for(symex_target_equationt::SSA_stepst::iterator
252 symex_target_equationt::SSA_stepst::iterator s_it=
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void slice_decl(SSA_stept &SSA_step)
The type of an expression, extends irept.
Single SSA step in the equation.
Base class for all expressions.
void simple_slice(symex_target_equationt &equation)
typet & type()
Return the type of the expression.
#define forall_operands(it, expr)
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
void slice(symex_target_equationt &equation)
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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.
std::unordered_set< irep_idt > symbol_sett
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
goto_trace_stept::typet type
void get_symbols(const exprt &expr)
API to expression classes.
void slice_assignment(SSA_stept &SSA_step)
void slice(symex_target_equationt &equation)