cprover
|
#include <static_analysis.h>
Public Member Functions | |
concurrency_aware_static_analysist (const namespacet &_ns) | |
virtual bool | merge_shared (static_analysis_baset::statet &a, const static_analysis_baset::statet &b, goto_programt::const_targett to) |
![]() | |
static_analysist (const namespacet &_ns) | |
T & | operator[] (locationt l) |
const T & | operator[] (locationt l) const |
virtual void | clear () |
virtual bool | has_location (locationt l) const |
![]() | |
static_analysis_baset (const namespacet &_ns) | |
virtual void | initialize (const goto_programt &goto_program) |
virtual void | initialize (const goto_functionst &goto_functions) |
virtual void | update (const goto_programt &goto_program) |
virtual void | update (const goto_functionst &goto_functions) |
virtual void | operator() (const goto_programt &goto_program) |
virtual void | operator() (const goto_functionst &goto_functions) |
virtual | ~static_analysis_baset () |
virtual void | output (const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_programt &goto_program, std::ostream &out) const |
void | insert (locationt l) |
Protected Member Functions | |
virtual void | fixedpoint (const goto_functionst &goto_functions) |
![]() | |
virtual statet & | get_state (locationt l) |
virtual const statet & | get_state (locationt l) const |
virtual bool | merge (statet &a, const statet &b, locationt to) |
virtual statet * | make_temporary_state (statet &s) |
virtual void | generate_state (locationt l) |
virtual void | get_reference_set (locationt l, const exprt &expr, std::list< exprt > &dest) |
![]() | |
virtual void | output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
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) |
void | sequential_fixedpoint (const goto_functionst &goto_functions) |
void | concurrent_fixedpoint (const goto_functionst &goto_functions) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions) |
void | generate_states (const goto_functionst &goto_functions) |
void | generate_states (const goto_programt &goto_program) |
void | do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions) |
void | 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, statet &new_state) |
Definition at line 372 of file static_analysis.h.
|
inlineexplicit |
Definition at line 376 of file static_analysis.h.
|
inlineprotectedvirtual |
Reimplemented from static_analysist< T >.
Definition at line 393 of file static_analysis.h.
References static_analysis_baset::concurrent_fixedpoint().
|
inlinevirtual |
Reimplemented from static_analysist< T >.
Definition at line 381 of file static_analysis.h.
References static_analysis_baset::ns.