|
cprover
|
#include <global_may_alias.h>
Protected Member Functions | |
| virtual void | initialize (const goto_functionst &_goto_functions) |
Protected Member Functions inherited from ait< global_may_alias_domaint > | |
| 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 |
Protected Member Functions inherited from ai_baset | |
| 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) |
Additional Inherited Members | |
Public Types inherited from ait< global_may_alias_domaint > | |
| typedef goto_programt::const_targett | locationt |
Public Types inherited from ai_baset | |
| typedef ai_domain_baset | statet |
| typedef goto_programt::const_targett | locationt |
Public Member Functions inherited from ait< global_may_alias_domaint > | |
| ait () | |
| global_may_alias_domaint & | operator[] (locationt l) |
| const global_may_alias_domaint & | operator[] (locationt l) const |
| void | clear () override |
Public Member Functions inherited from ai_baset | |
| 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 Types inherited from ait< global_may_alias_domaint > | |
| typedef std::unordered_map< locationt, global_may_alias_domaint, const_target_hash > | state_mapt |
Protected Types inherited from ai_baset | |
| typedef std::map< unsigned, locationt > | working_sett |
| typedef std::set< irep_idt > | recursion_sett |
Protected Attributes inherited from ait< global_may_alias_domaint > | |
| state_mapt | state_map |
Protected Attributes inherited from ai_baset | |
| recursion_sett | recursion_set |
Definition at line 75 of file global_may_alias.h.
|
inlineprotectedvirtual |
Reimplemented from ai_baset.
Definition at line 78 of file global_may_alias.h.