cprover
|
#include <static_analysis.h>
Public Types | |
typedef domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
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 | clear () |
virtual void | output (const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_programt &goto_program, std::ostream &out) const |
virtual bool | has_location (locationt l) const =0 |
void | insert (locationt l) |
Static Public Member Functions | |
static exprt | get_guard (locationt from, locationt to) |
static exprt | get_return_lhs (locationt to) |
Protected Types | |
typedef std::map< unsigned, locationt > | working_sett |
typedef std::set< irep_idt > | functions_donet |
typedef std::set< irep_idt > | recursion_sett |
typedef domain_baset::expr_sett | expr_sett |
Protected Member Functions | |
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) |
virtual void | fixedpoint (const goto_functionst &goto_functions)=0 |
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) |
virtual bool | merge (statet &a, const statet &b, locationt to)=0 |
virtual bool | merge_shared (statet &a, const statet &b, locationt to)=0 |
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) |
virtual void | generate_state (locationt l)=0 |
virtual statet & | get_state (locationt l)=0 |
virtual const statet & | get_state (locationt l) const =0 |
virtual std::unique_ptr< statet > | make_temporary_state (statet &s)=0 |
virtual void | get_reference_set (locationt l, const exprt &expr, std::list< exprt > &dest)=0 |
Static Protected Member Functions | |
static locationt | successor (locationt l) |
Protected Attributes | |
const namespacet & | ns |
functions_donet | functions_done |
recursion_sett | recursion_set |
bool | initialized |
Definition at line 97 of file static_analysis.h.
|
protected |
Definition at line 260 of file static_analysis.h.
|
protected |
Definition at line 224 of file static_analysis.h.
Definition at line 101 of file static_analysis.h.
|
protected |
Definition at line 227 of file static_analysis.h.
Definition at line 100 of file static_analysis.h.
|
protected |
Definition at line 182 of file static_analysis.h.
|
inlineexplicit |
Definition at line 103 of file static_analysis.h.
|
inlinevirtual |
Definition at line 138 of file static_analysis.h.
|
inlinevirtual |
Reimplemented in static_analysist< T >, and static_analysist< VSDT >.
Definition at line 142 of file static_analysis.h.
References initialized.
Referenced by static_analysist< VSDT >::clear().
|
protected |
Definition at line 430 of file static_analysis.cpp.
References goto_programt::add_instruction(), forall_goto_functions, forall_goto_program_instructions, generate_state(), get_next(), get_state(), goto_programt::instructions, merge(), merge_shared(), put_in_working_set(), sequential_fixedpoint(), and visit().
Referenced by concurrency_aware_static_analysist< T >::fixedpoint().
|
protected |
Definition at line 247 of file static_analysis.cpp.
References fixedpoint(), functions_done, get_state(), make_temporary_state(), merge(), ns, and domain_baset::transform().
Referenced by do_function_call_rec().
|
protected |
Definition at line 318 of file static_analysis.cpp.
References do_function_call(), goto_functionst::function_map, symbol_exprt::get_identifier(), get_reference_set(), id2string(), make_temporary_state(), merge(), object_descriptor_exprt::object(), recursion_set, to_object_descriptor_expr(), and to_symbol_expr().
Referenced by visit().
|
protected |
Definition at line 168 of file static_analysis.cpp.
References get_next(), goto_program, goto_programt::instructions, put_in_working_set(), and visit().
Referenced by do_function_call(), operator()(), and sequential_fixedpoint().
|
protectedpure virtual |
Implemented in concurrency_aware_static_analysist< T >, static_analysist< T >, and static_analysist< VSDT >.
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by concurrent_fixedpoint(), generate_states(), insert(), and update().
|
protected |
Definition at line 113 of file static_analysis.cpp.
References forall_goto_functions.
Referenced by initialize().
|
protected |
Definition at line 120 of file static_analysis.cpp.
References forall_goto_program_instructions, generate_state(), and goto_program.
Definition at line 23 of file static_analysis.cpp.
References exprt::make_not().
|
protected |
Definition at line 156 of file static_analysis.cpp.
Referenced by concurrent_fixedpoint(), and fixedpoint().
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by do_function_call_rec().
Definition at line 43 of file static_analysis.cpp.
References get_nil_irep(), and to_code_function_call().
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by concurrent_fixedpoint(), do_function_call(), output(), update(), and visit().
Implemented in static_analysist< T >, and static_analysist< VSDT >.
|
pure virtual |
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by update().
|
inlinevirtual |
Definition at line 109 of file static_analysis.h.
References generate_states(), goto_program, and initialized.
Referenced by operator()().
|
inlinevirtual |
Definition at line 119 of file static_analysis.h.
References generate_states(), and initialized.
|
inline |
Definition at line 160 of file static_analysis.h.
References generate_state().
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by do_function_call(), do_function_call_rec(), and visit().
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< VSDT >.
Referenced by concurrent_fixedpoint(), do_function_call(), do_function_call_rec(), update(), and visit().
|
protectedpure virtual |
Implemented in concurrency_aware_static_analysist< T >, static_analysist< T >, and static_analysist< VSDT >.
Referenced by concurrent_fixedpoint().
|
virtual |
Definition at line 68 of file static_analysis.cpp.
References fixedpoint(), goto_program, and initialize().
|
virtual |
Definition at line 61 of file static_analysis.cpp.
References fixedpoint(), and initialize().
|
virtual |
Definition at line 76 of file static_analysis.cpp.
References forall_goto_functions.
Referenced by output(), and show_value_sets().
|
inline |
Definition at line 151 of file static_analysis.h.
References goto_program, and output().
|
protectedvirtual |
Definition at line 94 of file static_analysis.cpp.
References forall_goto_program_instructions, get_state(), goto_program, ns, domain_baset::output(), and goto_programt::output_instruction().
|
inlineprotected |
Definition at line 186 of file static_analysis.h.
Referenced by concurrent_fixedpoint(), fixedpoint(), and visit().
|
protected |
Definition at line 420 of file static_analysis.cpp.
References fixedpoint(), forall_goto_functions, and functions_done.
Referenced by concurrent_fixedpoint(), and static_analysist< VSDT >::fixedpoint().
Definition at line 214 of file static_analysis.h.
|
virtual |
Definition at line 134 of file static_analysis.cpp.
References forall_goto_program_instructions, generate_state(), get_state(), goto_program, has_location(), and merge().
Referenced by update().
|
virtual |
Definition at line 127 of file static_analysis.cpp.
References forall_goto_functions, and update().
|
protected |
Definition at line 194 of file static_analysis.cpp.
References code_function_callt::arguments(), do_function_call_rec(), code_function_callt::function(), get_state(), goto_programt::get_successors(), goto_program, goto_programt::instructions, make_temporary_state(), merge(), ns, put_in_working_set(), domain_baset::seen, to_code_function_call(), and domain_baset::transform().
Referenced by concurrent_fixedpoint(), and fixedpoint().
|
protected |
Definition at line 225 of file static_analysis.h.
Referenced by do_function_call(), and sequential_fixedpoint().
|
protected |
Definition at line 236 of file static_analysis.h.
Referenced by clear(), and initialize().
|
protected |
Definition at line 175 of file static_analysis.h.
Referenced by do_function_call(), static_analysist< VSDT >::generate_state(), static_analysist< VSDT >::get_reference_set(), value_set_analysis_templatet< VSDT >::get_values(), concurrency_aware_static_analysist< T >::merge_shared(), output(), and visit().
|
protected |
Definition at line 228 of file static_analysis.h.
Referenced by do_function_call_rec().