12 #ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H 13 #define CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H 55 #endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H std::set< exprt > modifiest
function_modifiest(const goto_functionst &_goto_functions)
Goto Programs with Functions.
std::map< irep_idt, modifiest > function_mapt
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
void operator()(const exprt &function, modifiest &modifies)
instructionst::const_iterator const_targett
A collection of goto functions.
Base class for all expressions.
const goto_functionst & goto_functions
function_mapt function_map
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
void get_modifies_function(const exprt &, modifiest &)
Field-insensitive, location-sensitive may-alias analysis.