escape_analysist Class Reference
#include <escape_analysis.h>
Inheritance diagram for escape_analysist: Collaboration diagram for escape_analysist:Public Member Functions | |
| void | instrument (goto_modelt &) |
| Public Member Functions inherited from ait< escape_domaint > | |
| ait () | |
| escape_domaint & | operator[] (locationt l) |
| const escape_domaint & | operator[] (locationt l) const |
| std::unique_ptr< statet > | abstract_state_before (locationt t) const override |
| Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More... | |
| void | clear () override |
| Reset the abstract state. More... | |
| Public Member Functions inherited from ai_baset | |
| ai_baset () | |
| virtual | ~ai_baset () |
| void | operator() (const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns) |
| Run abstract interpretation on a single function. More... | |
| void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
| Run abstract interpretation on a whole program. More... | |
| void | operator() (const goto_modelt &goto_model) |
| Run abstract interpretation on a whole program. More... | |
| void | operator() (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| Run abstract interpretation on a single function. More... | |
| virtual std::unique_ptr< statet > | abstract_state_after (locationt l) const |
| Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More... | |
| virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
| Output the abstract states for a whole program. More... | |
| void | output (const goto_modelt &goto_model, std::ostream &out) const |
| Output the abstract states for a whole program. More... | |
| void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
| Output the abstract states for a function. More... | |
| void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
| Output the abstract states for a function. More... | |
| virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as JSON. More... | |
| jsont | output_json (const goto_modelt &goto_model) const |
| Output the abstract states for a whole program as JSON. More... | |
| jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as JSON. More... | |
| jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as JSON. More... | |
| virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as XML. More... | |
| xmlt | output_xml (const goto_modelt &goto_model) const |
| Output the abstract states for the whole program as XML. More... | |
| xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as XML. More... | |
| xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as XML. More... | |
Protected Member Functions | |
| virtual void | initialize (const goto_functionst &) |
| Initialize all the abstract states for a whole program. More... | |
| void | insert_cleanup (goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &) |
| Protected Member Functions inherited from ait< escape_domaint > | |
| virtual statet & | get_state (locationt l) override |
| Get the state for the given location, creating it in a default way if it doesn't exist. More... | |
| const statet & | find_state (locationt l) const override |
| Get the state for the given location if it already exists; throw an exception if it doesn't. More... | |
| bool | merge (const statet &src, locationt from, locationt to) override |
| std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
| Make a copy of a state. More... | |
| void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
| Protected Member Functions inherited from ai_baset | |
| virtual void | initialize (const goto_programt &goto_program) |
| Initialize all the abstract states for a single function. More... | |
| virtual void | initialize (const goto_functionst::goto_functiont &goto_function) |
| Initialize all the abstract states for a single function. More... | |
| virtual void | finalize () |
| Override this to add a cleanup or post-processing step after fixedpoint has run. More... | |
| void | entry_state (const goto_programt &goto_program) |
| Set the abstract state of the entry location of a single function to the entry state required by the analysis. More... | |
| void | entry_state (const goto_functionst &goto_functions) |
| Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More... | |
| virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
| Output the abstract states for a single function. More... | |
| virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the abstract states 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 abstract states for a single function as XML. More... | |
| locationt | get_next (working_sett &working_set) |
| Get the next location from the work queue. More... | |
| void | put_in_working_set (working_sett &working_set, locationt l) |
| bool | fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Run the fixedpoint algorithm until it reaches a fixed point. More... | |
| void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
| void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
| bool | visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Perform one step of abstract interpretation from location l Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More... | |
| bool | do_function_call_rec (const irep_idt &calling_function_identifier, 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 (const irep_idt &calling_function_identifier, 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 |
| Protected Attributes inherited from ait< escape_domaint > | |
| state_mapt | state_map |
Additional Inherited Members | |
| Public Types inherited from ait< escape_domaint > | |
| typedef goto_programt::const_targett | locationt |
| Public Types inherited from ai_baset | |
| typedef ai_domain_baset | statet |
| typedef goto_programt::const_targett | locationt |
| Protected Types inherited from ait< escape_domaint > | |
| typedef std::unordered_map< locationt, escape_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
| Protected Types inherited from ai_baset | |
| typedef std::map< unsigned, locationt > | working_sett |
| The work queue, sorted by location number. More... | |
Detailed Description
Definition at line 113 of file escape_analysis.h.
Member Function Documentation
◆ initialize()
|
inlineprotectedvirtual |
Initialize all the abstract states for a whole program.
Override this to do custom per-analysis initialization.
Reimplemented from ai_baset.
Definition at line 119 of file escape_analysis.h.
◆ insert_cleanup()
|
protected |
Definition at line 399 of file escape_analysis.cpp.
◆ instrument()
| void escape_analysist::instrument | ( | goto_modelt & | goto_model | ) |
Definition at line 434 of file escape_analysis.cpp.
Member Data Documentation
◆ bits
Definition at line 123 of file escape_analysis.h.
The documentation for this class was generated from the following files:
- analyses/escape_analysis.h
- analyses/escape_analysis.cpp
