45 const exprt &
function,
48 if(
function.
id()==ID_symbol)
52 function_mapt::const_iterator fm_it=
58 modifies.insert(fm_it->second.begin(), fm_it->second.end());
62 goto_functionst::function_mapt::const_iterator
75 else if(
function.
id()==ID_if)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const goto_functionst & goto_functions
function_mapt function_map
std::set< exprt > modifiest
void get_modifies_function(const exprt &, modifiest &)
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_function_call() const
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
const irep_idt & get_identifier() const
#define forall_goto_program_instructions(it, program)
Field-insensitive, location-sensitive may-alias analysis.
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
Helper functions for k-induction and loop invariants.
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.