28 locationt from{trace_from->current_location()};
35 const irep_idt &identifier = from->decl_symbol().get_identifier();
46 for(
const auto &expr : written)
50 for(
const auto &expr : read)
57 if(lhs.
id()==ID_index)
59 else if(lhs.
id()==ID_member)
61 else if(lhs.
id()==ID_symbol)
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const char * to_string() const
uninitializedt uninitialized
void assign(const exprt &lhs)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool merge(const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Detection for Uninitialized Local Variables.