cprover
static_analysist< T > Class Template Reference

#include <static_analysis.h>

+ Inheritance diagram for static_analysist< T >:
+ Collaboration diagram for static_analysist< T >:

Public Types

typedef goto_programt::const_targett locationt
 
- Public Types inherited from static_analysis_baset
typedef domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 static_analysist (const namespacet &_ns)
 
T & operator[] (locationt l)
 
const T & operator[] (locationt l) const
 
virtual void clear ()
 
virtual bool has_location (locationt l) const
 
- Public Member Functions inherited from static_analysis_baset
 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 irep_idt &function_identifier, 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)
 

Protected Types

typedef std::map< locationt, T > state_mapt
 
- Protected Types inherited from static_analysis_baset
typedef std::map< unsigned, locationtworking_sett
 
typedef std::set< irep_idtfunctions_donet
 
typedef std::set< irep_idtrecursion_sett
 
typedef domain_baset::expr_sett expr_sett
 

Protected Member Functions

virtual statetget_state (locationt l)
 
virtual const statetget_state (locationt l) const
 
virtual bool merge (statet &a, const statet &b, locationt to)
 
virtual std::unique_ptr< statetmake_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)
 
- Protected Member Functions inherited from static_analysis_baset
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 irep_idt &function_identifier, 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 (const irep_idt &function_identifier, 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 (const irep_idt &calling_function, 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 (const irep_idt &calling_function, 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)
 

Protected Attributes

state_mapt state_map
 
- Protected Attributes inherited from static_analysis_baset
const namespacetns
 
functions_donet functions_done
 
recursion_sett recursion_set
 
bool initialized
 

Private Member Functions

void dummy (const T &s)
 
virtual bool merge_shared (statet &, const statet &, goto_programt::const_targett)
 

Additional Inherited Members

- Static Public Member Functions inherited from static_analysis_baset
static exprt get_guard (locationt from, locationt to)
 
static exprt get_return_lhs (locationt to)
 
- Static Protected Member Functions inherited from static_analysis_baset
static locationt successor (locationt l)
 

Detailed Description

template<typename T>
class static_analysist< T >

Definition at line 279 of file static_analysis.h.

Member Typedef Documentation

◆ locationt

template<typename T>
typedef goto_programt::const_targett static_analysist< T >::locationt

Definition at line 288 of file static_analysis.h.

◆ state_mapt

template<typename T>
typedef std::map<locationt, T> static_analysist< T >::state_mapt
protected

Definition at line 320 of file static_analysis.h.

Constructor & Destructor Documentation

◆ static_analysist()

template<typename T>
static_analysist< T >::static_analysist ( const namespacet _ns)
inlineexplicit

Definition at line 283 of file static_analysis.h.

Member Function Documentation

◆ clear()

template<typename T>
virtual void static_analysist< T >::clear ( void  )
inlinevirtual

Reimplemented from static_analysis_baset.

Definition at line 308 of file static_analysis.h.

◆ dummy()

template<typename T>
void static_analysist< T >::dummy ( const T &  s)
inlineprivate

Definition at line 371 of file static_analysis.h.

◆ fixedpoint()

template<typename T>
virtual void static_analysist< T >::fixedpoint ( const goto_functionst goto_functions)
inlineprotectedvirtual

Implements static_analysis_baset.

Reimplemented in concurrency_aware_static_analysist< T >.

Definition at line 364 of file static_analysis.h.

◆ generate_state()

template<typename T>
virtual void static_analysist< T >::generate_state ( locationt  l)
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 351 of file static_analysis.h.

◆ get_reference_set()

template<typename T>
virtual void static_analysist< T >::get_reference_set ( locationt  l,
const exprt expr,
std::list< exprt > &  dest 
)
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 356 of file static_analysis.h.

◆ get_state() [1/2]

template<typename T>
virtual statet& static_analysist< T >::get_state ( locationt  l)
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 323 of file static_analysis.h.

◆ get_state() [2/2]

template<typename T>
virtual const statet& static_analysist< T >::get_state ( locationt  l) const
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 332 of file static_analysis.h.

◆ has_location()

template<typename T>
virtual bool static_analysist< T >::has_location ( locationt  l) const
inlinevirtual

Implements static_analysis_baset.

Definition at line 314 of file static_analysis.h.

◆ make_temporary_state()

template<typename T>
virtual std::unique_ptr<statet> static_analysist< T >::make_temporary_state ( statet s)
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 346 of file static_analysis.h.

◆ merge()

template<typename T>
virtual bool static_analysist< T >::merge ( statet a,
const statet b,
locationt  to 
)
inlineprotectedvirtual

Implements static_analysis_baset.

Definition at line 341 of file static_analysis.h.

◆ merge_shared()

template<typename T>
virtual bool static_analysist< T >::merge_shared ( statet ,
const statet ,
goto_programt::const_targett   
)
inlineprivatevirtual

Implements static_analysis_baset.

Reimplemented in concurrency_aware_static_analysist< T >.

Definition at line 374 of file static_analysis.h.

◆ operator[]() [1/2]

template<typename T>
T& static_analysist< T >::operator[] ( locationt  l)
inline

Definition at line 290 of file static_analysis.h.

◆ operator[]() [2/2]

template<typename T>
const T& static_analysist< T >::operator[] ( locationt  l) const
inline

Definition at line 299 of file static_analysis.h.

Member Data Documentation

◆ state_map

template<typename T>
state_mapt static_analysist< T >::state_map
protected

Definition at line 321 of file static_analysis.h.


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