cprover
|
#include <reaching_definitions.h>
Public Member Functions | |
reaching_definitions_analysist (const namespacet &_ns) | |
virtual | ~reaching_definitions_analysist () |
virtual void | initialize (const goto_functionst &goto_functions) override |
virtual statet & | get_state (goto_programt::const_targett l) override |
value_setst & | get_value_sets () const |
const is_threadedt & | get_is_threaded () const |
const dirtyt & | get_is_dirty () const |
![]() | |
concurrency_aware_ait () | |
bool | merge_shared (const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override |
![]() | |
ait () | |
rd_range_domaint & | operator[] (locationt l) |
const rd_range_domaint & | operator[] (locationt l) const |
std::unique_ptr< statet > | abstract_state_before (locationt t) const override |
Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc. More... | |
void | clear () override |
Resets the domain. More... | |
![]() | |
ai_baset () | |
virtual | ~ai_baset () |
void | operator() (const goto_programt &goto_program, const namespacet &ns) |
Running the interpreter. More... | |
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
void | operator() (const goto_modelt &goto_model) |
void | operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
virtual std::unique_ptr< statet > | abstract_state_after (locationt l) const |
Returns the abstract state after the given instruction. More... | |
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_modelt &goto_model, std::ostream &out) const |
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as JSON. More... | |
jsont | output_json (const goto_modelt &goto_model) const |
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as XML. More... | |
xmlt | output_xml (const goto_modelt &goto_model) const |
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
![]() | |
const reaching_definitiont & | get (const std::size_t value_index) const |
std::size_t | add (const reaching_definitiont &value) |
void | clear () |
Protected Attributes | |
const namespacet & | ns |
std::unique_ptr< value_setst > | value_sets |
std::unique_ptr< is_threadedt > | is_threaded |
std::unique_ptr< dirtyt > | is_dirty |
![]() | |
state_mapt | state_map |
![]() | |
std::vector< typename inner_mapt::const_iterator > | values |
std::unordered_map< irep_idt, inner_mapt > | value_map |
Additional Inherited Members | |
![]() | |
typedef ait< rd_range_domaint >::statet | statet |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef ai_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef std::unordered_map< locationt, rd_range_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
![]() | |
typedef std::map< unsigned, locationt > | working_sett |
![]() | |
typedef std::map< reaching_definitiont, std::size_t > | inner_mapt |
![]() | |
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
![]() | |
const statet & | find_state (locationt l) const override |
bool | merge (const statet &src, locationt from, locationt to) override |
std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
![]() | |
virtual void | initialize (const goto_programt &) |
virtual void | initialize (const goto_functionst::goto_functiont &) |
virtual void | finalize () |
void | entry_state (const goto_programt &) |
void | entry_state (const goto_functionst &) |
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as JSON. More... | |
virtual xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as XML. More... | |
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, const namespacet &ns) |
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns) |
bool | 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, const namespacet &ns) |
Definition at line 249 of file reaching_definitions.h.
|
explicit |
Definition at line 29 of file reaching_definitions.cpp.
|
virtualdefault |
|
inline |
Definition at line 289 of file reaching_definitions.h.
References is_dirty.
Referenced by rd_range_domaint::transform(), rd_range_domaint::transform_assign(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), and rd_range_domaint::transform_start_thread().
|
inline |
Definition at line 283 of file reaching_definitions.h.
References is_threaded.
Referenced by rd_range_domaint::transform(), rd_range_domaint::transform_assign(), and rd_range_domaint::transform_end_function().
|
inlineoverridevirtual |
Reimplemented from ait< rd_range_domaint >.
Definition at line 262 of file reaching_definitions.h.
References ait< domainT >::get_state(), INVARIANT_STRUCTURED, and rd_range_domaint::set_bitvector_container().
Referenced by rd_range_domaint::transform_end_function().
|
inline |
Definition at line 277 of file reaching_definitions.h.
References value_sets.
Referenced by dep_graph_domaint::data_dependencies(), rd_range_domaint::transform(), and rd_range_domaint::transform_assign().
|
overridevirtual |
Reimplemented from ai_baset.
Definition at line 729 of file reaching_definitions.cpp.
References ai_baset::initialize(), is_dirty, is_threaded, ns, and value_sets.
|
protected |
Definition at line 299 of file reaching_definitions.h.
Referenced by get_is_dirty(), and initialize().
|
protected |
Definition at line 298 of file reaching_definitions.h.
Referenced by get_is_threaded(), and initialize().
|
protected |
Definition at line 296 of file reaching_definitions.h.
Referenced by initialize().
|
protected |
Definition at line 297 of file reaching_definitions.h.
Referenced by get_value_sets(), and initialize().