18 bool unchanged =
true;
25 const auto &
id = it->id();
35 .with_source_location(*it);
39 it.next_sibling_or_parent();
52 .with_source_location(*it);
56 it.next_sibling_or_parent();
65 return std::move(expr);
72 for(
auto &instruction : goto_function.body.instructions)
73 instruction.transform(
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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().
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
A base class for a predicate that indicates that an address range is ok to read or write or both.
Forward depth-first search iterators These iterators' copy operations are expensive,...
API to expression classes for Pointers.
static std::optional< exprt > rewrite_rw_ok(exprt expr, const namespacet &ns)
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.