cprover
|
#include <escape_analysis.h>
Public Member Functions | |
void | instrument (goto_functionst &, const namespacet &) |
![]() | |
ait () | |
escape_domaint & | operator[] (locationt l) |
const escape_domaint & | operator[] (locationt l) const |
void | clear () override |
![]() | |
ai_baset () | |
virtual | ~ai_baset () |
void | operator() (const goto_programt &goto_program, const namespacet &ns) |
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
void | operator() (const goto_modelt &goto_model) |
void | operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_modelt &goto_model, std::ostream &out) const |
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as JSON. More... | |
jsont | output_json (const goto_modelt &goto_model) const |
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as XML. More... | |
xmlt | output_xml (const goto_modelt &goto_model) const |
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
Protected Member Functions | |
virtual void | initialize (const goto_functionst &_goto_functions) |
void | insert_cleanup (goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &) |
![]() | |
virtual statet & | get_state (locationt l) override |
const statet & | find_state (locationt l) const override |
bool | merge (const statet &src, locationt from, locationt to) override |
statet * | make_temporary_state (const statet &s) override |
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
![]() | |
virtual void | initialize (const goto_programt &) |
virtual void | initialize (const goto_functionst::goto_functiont &) |
void | entry_state (const goto_programt &) |
void | entry_state (const goto_functionst &) |
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as JSON. More... | |
virtual xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as XML. More... | |
locationt | get_next (working_sett &working_set) |
void | put_in_working_set (working_sett &working_set, locationt l) |
bool | fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call (locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns) |
Protected Attributes | |
numbering< irep_idt > | bits |
![]() | |
state_mapt | state_map |
![]() | |
recursion_sett | recursion_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef ai_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef std::unordered_map< locationt, escape_domaint, const_target_hash > | state_mapt |
![]() | |
typedef std::map< unsigned, locationt > | working_sett |
typedef std::set< irep_idt > | recursion_sett |
Definition at line 95 of file escape_analysis.h.
|
inlineprotectedvirtual |
Reimplemented from ai_baset.
Definition at line 103 of file escape_analysis.h.
|
protected |
Definition at line 401 of file escape_analysis.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), code_function_callt::function(), code_function_callt::lhs(), namespacet::lookup(), irept::make_nil(), exprt::make_typecast(), code_typet::parameters(), to_code_type(), and exprt::type().
void escape_analysist::instrument | ( | goto_functionst & | goto_functions, |
const namespacet & | ns | ||
) |
Definition at line 438 of file escape_analysis.cpp.
References ASSIGN, escape_domaint::check_lhs(), escape_domaint::cleanup_map, DEAD, Forall_goto_functions, Forall_goto_program_instructions, code_deadt::get_identifier(), id2string(), code_assignt::lhs(), code_deadt::symbol(), to_code_assign(), and to_code_dead().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
Definition at line 107 of file escape_analysis.h.