cprover
|
#include <value_set_analysis.h>
Public Types | |
typedef static_analysist< value_set_domaint > | baset |
![]() | |
typedef std::list< exprt > | valuest |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
value_set_analysist (const namespacet &_ns) | |
virtual void | initialize (const goto_programt &goto_program) |
virtual void | initialize (const goto_functionst &goto_functions) |
void | convert (const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const |
virtual void | get_values (locationt l, const exprt &expr, value_setst::valuest &dest) |
![]() | |
value_setst () | |
virtual | ~value_setst () |
![]() | |
static_analysist (const namespacet &_ns) | |
value_set_domaint & | operator[] (locationt l) |
const value_set_domaint & | operator[] (locationt l) const |
virtual void | clear () |
virtual bool | has_location (locationt l) const |
![]() | |
static_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 | ~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) |
Additional Inherited Members | |
![]() | |
static exprt | get_guard (locationt from, locationt to) |
static exprt | get_return_lhs (locationt to) |
![]() | |
typedef std::map< locationt, value_set_domaint > | state_mapt |
![]() | |
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 |
![]() | |
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 | fixedpoint (const goto_functionst &goto_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) |
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) |
![]() | |
static locationt | successor (locationt l) |
![]() | |
state_mapt | state_map |
![]() | |
const namespacet & | ns |
functions_donet | functions_done |
recursion_sett | recursion_set |
bool | initialized |
Definition at line 23 of file value_set_analysis.h.
Definition at line 33 of file value_set_analysis.h.
|
inlineexplicit |
Definition at line 28 of file value_set_analysis.h.
void value_set_analysist::convert | ( | const goto_programt & | goto_program, |
const irep_idt & | identifier, | ||
xmlt & | dest | ||
) | const |
Definition at line 33 of file value_set_analysis.cpp.
References xmlt::data, dstringt::empty(), xmlt::escape(), forall_goto_program_instructions, from_expr(), source_locationt::get_file(), id2string(), irept::is_nil(), xmlt::new_element(), static_analysis_baset::ns, value_sett::values, and xml().
Referenced by convert(), and get_values().
|
inlinevirtual |
Implements value_setst.
Definition at line 46 of file value_set_analysis.h.
References convert(), and static_analysis_baset::ns.
|
virtual |
Reimplemented from static_analysis_baset.
Definition at line 21 of file value_set_analysis.cpp.
References static_analysis_baset::initialize().
|
virtual |
Reimplemented from static_analysis_baset.
Definition at line 27 of file value_set_analysis.cpp.
References static_analysis_baset::initialize().