cprover
reaching_definitions_analysist Class Reference

#include <reaching_definitions.h>

Inheritance diagram for reaching_definitions_analysist:
[legend]
Collaboration diagram for reaching_definitions_analysist:
[legend]

Public Member Functions

 reaching_definitions_analysist (const namespacet &_ns)
 
virtual ~reaching_definitions_analysist ()
 
virtual void initialize (const goto_functionst &goto_functions)
 
virtual statetget_state (goto_programt::const_targett l)
 
value_setstget_value_sets () const
 
const is_threadedtget_is_threaded () const
 
const dirtytget_is_dirty () const
 
- Public Member Functions inherited from concurrency_aware_ait< rd_range_domaint >
 concurrency_aware_ait ()
 
bool merge_shared (const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
 
- Public Member Functions inherited from ait< rd_range_domaint >
 ait ()
 
rd_range_domaintoperator[] (locationt l)
 
const rd_range_domaintoperator[] (locationt l) const
 
void clear () override
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const goto_programt &goto_program, const namespacet &ns)
 
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 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
 
- Public Member Functions inherited from sparse_bitvector_analysist< reaching_definitiont >
const reaching_definitiontget (const std::size_t value_index) const
 
std::size_t add (const reaching_definitiont &value)
 
void clear ()
 

Protected Attributes

const namespacetns
 
value_setstvalue_sets
 
is_threadedtis_threaded
 
dirtytis_dirty
 
- Protected Attributes inherited from ait< rd_range_domaint >
state_mapt state_map
 
- Protected Attributes inherited from ai_baset
recursion_sett recursion_set
 
- Protected Attributes inherited from sparse_bitvector_analysist< reaching_definitiont >
std::vector< typename inner_mapt::const_iterator > values
 
std::unordered_map< irep_idt, inner_mapt, irep_id_hashvalue_map
 

Additional Inherited Members

- Public Types inherited from concurrency_aware_ait< rd_range_domaint >
typedef ait< rd_range_domaint >::statet statet
 
- Public Types inherited from ait< rd_range_domaint >
typedef goto_programt::const_targett locationt
 
- Public Types inherited from ai_baset
typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 
- Protected Types inherited from ait< rd_range_domaint >
typedef std::unordered_map< locationt, rd_range_domaint, const_target_hashstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 
typedef std::set< irep_idtrecursion_sett
 
- Protected Types inherited from sparse_bitvector_analysist< reaching_definitiont >
typedef std::map< reaching_definitiont, std::size_t > inner_mapt
 
- Protected Member Functions inherited from concurrency_aware_ait< rd_range_domaint >
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ait< rd_range_domaint >
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
statetmake_temporary_state (const statet &s) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const goto_programt &)
 
virtual void initialize (const goto_functionst::goto_functiont &)
 
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)
 

Detailed Description

Definition at line 238 of file reaching_definitions.h.

Constructor & Destructor Documentation

§ reaching_definitions_analysist()

reaching_definitions_analysist::reaching_definitions_analysist ( const namespacet _ns)
inlineexplicit

Definition at line 244 of file reaching_definitions.h.

§ ~reaching_definitions_analysist()

reaching_definitions_analysist::~reaching_definitions_analysist ( )
virtual

Definition at line 720 of file reaching_definitions.cpp.

Member Function Documentation

§ get_is_dirty()

§ get_is_threaded()

const is_threadedt& reaching_definitions_analysist::get_is_threaded ( ) const
inline

§ get_state()

virtual statet& reaching_definitions_analysist::get_state ( goto_programt::const_targett  l)
inlinevirtual

§ get_value_sets()

value_setst& reaching_definitions_analysist::get_value_sets ( ) const
inline

§ initialize()

void reaching_definitions_analysist::initialize ( const goto_functionst goto_functions)
virtual

Reimplemented from ai_baset.

Definition at line 730 of file reaching_definitions.cpp.

References ai_baset::initialize().

Member Data Documentation

§ is_dirty

dirtyt* reaching_definitions_analysist::is_dirty
protected

Definition at line 295 of file reaching_definitions.h.

§ is_threaded

is_threadedt* reaching_definitions_analysist::is_threaded
protected

Definition at line 294 of file reaching_definitions.h.

§ ns

const namespacet& reaching_definitions_analysist::ns
protected

Definition at line 292 of file reaching_definitions.h.

§ value_sets

value_setst* reaching_definitions_analysist::value_sets
protected

Definition at line 293 of file reaching_definitions.h.


The documentation for this class was generated from the following files: