Go to the documentation of this file.
41 code_function_call.
function(), modifies);
46 const exprt &
function,
49 if(
function.
id()==ID_symbol)
53 function_mapt::const_iterator fm_it=
59 modifies.insert(fm_it->second.begin(), fm_it->second.end());
63 goto_functionst::function_mapt::const_iterator
76 else if(
function.
id()==ID_if)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
function_mapt function_map
Base class for all expressions.
const goto_functionst & goto_functions
function_mapt function_map
codet representation of a function call statement.
codet code
Do not read or modify directly – use get_X() instead.
const irep_idt & get_identifier() const
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_function_callt & to_code_function_call(const codet &code)
Helper functions for k-induction and loop invariants.
const code_assignt & to_code_assign(const codet &code)
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool is_function_call() const
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
#define forall_goto_program_instructions(it, program)
std::set< exprt > modifiest
void get_modifies_function(const exprt &, modifiest &)