cprover
|
#include <value_set_analysis_fivr.h>
Public Types | |
enum | track_optionst { TRACK_ALL_POINTERS, TRACK_FUNCTION_POINTERS } |
typedef flow_insensitive_analysist< value_set_domain_fivrt > | baset |
![]() | |
typedef std::list< exprt > | valuest |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef flow_insensitive_abstract_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
value_set_analysis_fivrt (const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS) | |
virtual void | initialize (const goto_programt &goto_program) |
virtual void | initialize (const goto_functionst &goto_functions) |
void | output (locationt l, std::ostream &out) |
void | output (const goto_programt &goto_program, std::ostream &out) |
virtual void | get_values (locationt l, const exprt &expr, std::list< exprt > &dest) |
![]() | |
value_setst () | |
virtual | ~value_setst () |
![]() | |
flow_insensitive_analysist (const namespacet &_ns) | |
virtual void | clear () |
value_set_domain_fivrt & | get_data () |
const value_set_domain_fivrt & | get_data () const |
![]() | |
bool | seen (const locationt &l) |
flow_insensitive_analysis_baset (const namespacet &_ns) | |
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 | ~flow_insensitive_analysis_baset () |
virtual void | output (const goto_functionst &goto_functions, std::ostream &out) |
Protected Member Functions | |
bool | check_type (const typet &type) |
void | get_globals (std::list< value_set_fivrt::entryt > &dest) |
void | add_vars (const goto_functionst &goto_functions) |
void | add_vars (const goto_programt &goto_programa) |
void | get_entries (const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest) |
void | get_entries_rec (const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest) |
![]() | |
virtual statet & | get_state () |
virtual const statet & | get_state () const |
void | get_reference_set (const exprt &expr, expr_sett &expr_set) |
![]() | |
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) |
bool | fixedpoint (goto_functionst::function_mapt::const_iterator it, const goto_functionst &goto_functions) |
void | fixedpoint (const goto_functionst &goto_functions) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions) |
bool | do_function_call_rec (locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions) |
bool | do_function_call (locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state) |
Protected Attributes | |
track_optionst | track_options |
![]() | |
value_set_domain_fivrt | state |
![]() | |
const namespacet & | ns |
functions_donet | functions_done |
recursion_sett | recursion_set |
bool | initialized |
Additional Inherited Members | |
![]() | |
std::set< locationt > | seen_locations |
std::map< locationt, unsigned > | statistics |
![]() | |
typedef std::priority_queue< locationt > | working_sett |
typedef std::set< irep_idt > | functions_donet |
typedef std::set< irep_idt > | recursion_sett |
typedef flow_insensitive_abstract_domain_baset::expr_sett | expr_sett |
![]() | |
static locationt | successor (locationt l) |
Definition at line 20 of file value_set_analysis_fivr.h.
Definition at line 36 of file value_set_analysis_fivr.h.
Enumerator | |
---|---|
TRACK_ALL_POINTERS | |
TRACK_FUNCTION_POINTERS |
Definition at line 25 of file value_set_analysis_fivr.h.
|
inline |
Definition at line 28 of file value_set_analysis_fivr.h.
|
protected |
Definition at line 118 of file value_set_analysis_fivr.cpp.
References value_set_fivrt::add_vars(), forall_goto_functions, get_entries(), get_globals(), get_local_identifiers(), namespacet::lookup(), flow_insensitive_analysis_baset::ns, flow_insensitive_analysist< value_set_domain_fivrt >::state, and value_set_domain_fivrt::value_set.
Referenced by initialize().
|
protected |
Definition at line 36 of file value_set_analysis_fivr.cpp.
References value_set_fivrt::add_vars(), goto_programt::get_decl_identifiers(), get_entries(), get_globals(), goto_program, namespacet::lookup(), flow_insensitive_analysis_baset::ns, flow_insensitive_analysist< value_set_domain_fivrt >::state, and value_set_domain_fivrt::value_set.
|
protected |
Definition at line 158 of file value_set_analysis_fivr.cpp.
References struct_union_typet::components(), namespace_baset::follow(), irept::id(), flow_insensitive_analysis_baset::ns, typet::subtype(), to_struct_type(), TRACK_ALL_POINTERS, TRACK_FUNCTION_POINTERS, and track_options.
Referenced by get_entries_rec().
|
protected |
Definition at line 74 of file value_set_analysis_fivr.cpp.
References get_entries_rec(), symbolt::name, and symbolt::type.
Referenced by add_vars(), and get_globals().
|
protected |
Definition at line 81 of file value_set_analysis_fivr.cpp.
References check_type(), struct_union_typet::components(), namespace_baset::follow(), irept::id(), flow_insensitive_analysis_baset::ns, typet::subtype(), and to_struct_type().
Referenced by get_entries().
|
protected |
Definition at line 145 of file value_set_analysis_fivr.cpp.
References get_entries(), namespacet::get_symbol_table(), flow_insensitive_analysis_baset::ns, and symbol_table_baset::symbols.
Referenced by add_vars().
|
inlinevirtual |
Implements value_setst.
Definition at line 81 of file value_set_analysis_fivr.h.
References value_set_fivrt::from_function, value_set_fivrt::from_target_index, value_set_fivrt::function_numbering, value_set_fivrt::get_value_set(), flow_insensitive_analysis_baset::ns, flow_insensitive_analysist< value_set_domain_fivrt >::state, value_set_fivrt::to_function, value_set_fivrt::to_target_index, and value_set_domain_fivrt::value_set.
|
virtual |
Reimplemented from flow_insensitive_analysis_baset.
Definition at line 22 of file value_set_analysis_fivr.cpp.
References add_vars(), goto_program, and flow_insensitive_analysis_baset::initialize().
|
virtual |
Reimplemented from flow_insensitive_analysis_baset.
Definition at line 29 of file value_set_analysis_fivr.cpp.
References add_vars(), and flow_insensitive_analysis_baset::initialize().
|
inline |
Definition at line 42 of file value_set_analysis_fivr.h.
References flow_insensitive_analysis_baset::ns, value_set_domain_fivrt::output(), value_set_fivrt::set_from(), value_set_fivrt::set_to(), flow_insensitive_analysist< value_set_domain_fivrt >::state, and value_set_domain_fivrt::value_set.
Referenced by output().
|
inlinevirtual |
Reimplemented from flow_insensitive_analysis_baset.
Definition at line 49 of file value_set_analysis_fivr.h.
References forall_goto_program_instructions, goto_program, flow_insensitive_analysis_baset::ns, output(), and goto_programt::output_instruction().
|
protected |
Definition at line 62 of file value_set_analysis_fivr.h.
Referenced by check_type().