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 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 94 of file static_analysis.h.
|
protected |
Definition at line 257 of file static_analysis.h.
|
protected |
Definition at line 221 of file static_analysis.h.
Definition at line 98 of file static_analysis.h.
|
protected |
Definition at line 224 of file static_analysis.h.
Definition at line 97 of file static_analysis.h.
|
protected |
Definition at line 179 of file static_analysis.h.
|
inlineexplicit |
Definition at line 100 of file static_analysis.h.
|
inlinevirtual |
Definition at line 135 of file static_analysis.h.
|
inlinevirtual |
Reimplemented in static_analysist< T >, and static_analysist< value_set_domaint >.
Definition at line 139 of file static_analysis.h.
References domain_baset::output().
Referenced by static_analysist< value_set_domaint >::clear().
|
protected |
Definition at line 430 of file static_analysis.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), forall_goto_functions, forall_goto_program_instructions, generate_state(), get_next(), get_state(), goto_program_templatet< codeT, guardT >::instructions, merge(), merge_shared(), put_in_working_set(), sequential_fixedpoint(), and visit().
|
protected |
Definition at line 247 of file static_analysis.cpp.
References goto_function_templatet< bodyT >::body, goto_function_templatet< bodyT >::body_available(), 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_functions_templatet< bodyT >::function_map, get_reference_set(), id2string(), make_temporary_state(), merge(), object_descriptor_exprt::object(), recursion_set, and to_object_descriptor_expr().
Referenced by visit().
|
protected |
Definition at line 168 of file static_analysis.cpp.
References get_next(), goto_program_templatet< codeT, guardT >::instructions, put_in_working_set(), and visit().
Referenced by do_function_call(), operator()(), and sequential_fixedpoint().
|
protectedpure virtual |
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
Referenced by concurrent_fixedpoint(), generate_states(), and update().
|
protected |
Definition at line 113 of file static_analysis.cpp.
References forall_goto_functions.
|
protected |
Definition at line 120 of file static_analysis.cpp.
References forall_goto_program_instructions, and generate_state().
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< value_set_domaint >.
Referenced by do_function_call_rec().
Definition at line 43 of file static_analysis.cpp.
References get_nil_irep(), and to_code_function_call().
Referenced by value_set_domaint::transform().
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
Referenced by concurrent_fixedpoint(), do_function_call(), output(), update(), and visit().
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
|
pure virtual |
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
Referenced by update().
|
inlinevirtual |
Reimplemented in value_set_analysist.
Definition at line 106 of file static_analysis.h.
Referenced by value_set_analysist::initialize(), and operator()().
|
inlinevirtual |
Reimplemented in value_set_analysist.
Definition at line 116 of file static_analysis.h.
|
inline |
Definition at line 157 of file static_analysis.h.
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
Referenced by do_function_call(), do_function_call_rec(), and visit().
|
protectedpure virtual |
Implemented in static_analysist< T >, and static_analysist< value_set_domaint >.
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< value_set_domaint >.
Referenced by concurrent_fixedpoint().
|
virtual |
Definition at line 68 of file static_analysis.cpp.
References fixedpoint(), 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 show_value_sets().
|
inline |
Definition at line 148 of file static_analysis.h.
References domain_baset::output().
|
protectedvirtual |
Definition at line 94 of file static_analysis.cpp.
References forall_goto_program_instructions, get_state(), ns, domain_baset::output(), and goto_programt::output_instruction().
|
inlineprotected |
Definition at line 183 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().
Definition at line 211 of file static_analysis.h.
|
virtual |
Definition at line 134 of file static_analysis.cpp.
References forall_goto_program_instructions, generate_state(), get_state(), 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_program_templatet< codeT, guardT >::get_successors(), goto_program_templatet< codeT, guardT >::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 222 of file static_analysis.h.
Referenced by do_function_call(), and sequential_fixedpoint().
|
protected |
Definition at line 233 of file static_analysis.h.
|
protected |
Definition at line 172 of file static_analysis.h.
Referenced by value_sett::apply_code(), value_sett::assign(), value_sett::assign_rec(), value_set_analysist::convert(), do_function_call(), value_sett::eval_pointer_offset(), value_sett::get_reference_set_rec(), value_sett::get_value_set(), value_sett::get_value_set_rec(), value_set_analysist::get_values(), value_sett::guard(), value_sett::make_member(), output(), and visit().
|
protected |
Definition at line 225 of file static_analysis.h.
Referenced by do_function_call_rec().