cprover
|
#include <function_modifies.h>
Public Types | |
typedef std::set< exprt > | modifiest |
Public Member Functions | |
function_modifiest (const goto_functionst &_goto_functions) | |
void | get_modifies (const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &) |
void | get_modifies_lhs (const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &) |
void | get_modifies_function (const exprt &, modifiest &) |
void | operator() (const exprt &function, modifiest &modifies) |
Protected Types | |
typedef std::map< irep_idt, modifiest > | function_mapt |
Protected Attributes | |
const goto_functionst & | goto_functions |
function_mapt | function_map |
Definition at line 18 of file function_modifies.h.
|
protected |
Definition at line 51 of file function_modifies.h.
typedef std::set<exprt> function_modifiest::modifiest |
Definition at line 26 of file function_modifies.h.
|
inlineexplicit |
Definition at line 21 of file function_modifies.h.
void function_modifiest::get_modifies | ( | const local_may_aliast & | local_may_alias, |
const goto_programt::const_targett | i_it, | ||
modifiest & | modifies | ||
) |
Definition at line 45 of file function_modifies.cpp.
References code_function_callt::function(), get_modifies_function(), get_modifies_lhs(), irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), to_code_assign(), and to_code_function_call().
Referenced by get_modifies_function().
Definition at line 72 of file function_modifies.cpp.
References forall_goto_program_instructions, function_map, goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), get_modifies(), goto_functions, to_if_expr(), and to_symbol_expr().
Referenced by get_modifies(), and operator()().
void function_modifiest::get_modifies_lhs | ( | const local_may_aliast & | local_may_alias, |
const goto_programt::const_targett | t, | ||
const exprt & | lhs, | ||
modifiest & | modifies | ||
) |
Definition at line 16 of file function_modifies.cpp.
References local_may_aliast::get(), irept::id(), code_function_callt::lhs(), to_dereference_expr(), and to_if_expr().
Referenced by get_modifies(), and havoc_loopst::get_modifies().
Definition at line 43 of file function_modifies.h.
References get_modifies_function().
|
protected |
Definition at line 52 of file function_modifies.h.
Referenced by get_modifies_function().
|
protected |
Definition at line 49 of file function_modifies.h.
Referenced by get_modifies_function().