cprover
ait< domainT > Class Template Reference

#include <ai.h>

Inheritance diagram for ait< domainT >:
[legend]
Collaboration diagram for ait< domainT >:
[legend]

Public Types

typedef goto_programt::const_targett locationt
 
- Public Types inherited from ai_baset
typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 ait ()
 
domainT & operator[] (locationt l)
 
const domainT & operator[] (locationt l) const
 
std::unique_ptr< statetabstract_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...
 
- Public Member Functions inherited from ai_baset
 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< statetabstract_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
 

Protected Types

typedef std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equaltstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 

Protected Member Functions

virtual statetget_state (locationt l) override
 
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
std::unique_ptr< statetmake_temporary_state (const statet &s) override
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const goto_programt &)
 
virtual void initialize (const goto_functionst::goto_functiont &)
 
virtual void initialize (const goto_functionst &)
 
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)
 

Protected Attributes

state_mapt state_map
 

Private Member Functions

void dummy (const domainT &s)
 
bool merge_shared (const statet &, goto_programt::const_targett, goto_programt::const_targett, const namespacet &) override
 

Detailed Description

template<typename domainT>
class ait< domainT >

Definition at line 294 of file ai.h.

Member Typedef Documentation

◆ locationt

template<typename domainT>
typedef goto_programt::const_targett ait< domainT >::locationt

Definition at line 302 of file ai.h.

◆ state_mapt

template<typename domainT>
typedef std:: unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt> ait< domainT >::state_mapt
protected

Definition at line 344 of file ai.h.

Constructor & Destructor Documentation

◆ ait()

template<typename domainT>
ait< domainT >::ait ( )
inline

Definition at line 298 of file ai.h.

Member Function Documentation

◆ abstract_state_before()

template<typename domainT>
std::unique_ptr<statet> ait< domainT >::abstract_state_before ( locationt  l) const
inlineoverridevirtual

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.

Intended for users of the abstract interpreter; don't use internally. Returns the abstract state before the given instruction PRECONDITION(l is dereferenceable)

Implements ai_baset.

Definition at line 322 of file ai.h.

◆ clear()

template<typename domainT>
void ait< domainT >::clear ( )
inlineoverridevirtual

Resets the domain.

Reimplemented from ai_baset.

Definition at line 335 of file ai.h.

◆ dummy()

template<typename domainT>
void ait< domainT >::dummy ( const domainT &  s)
inlineprivate

Definition at line 384 of file ai.h.

◆ find_state()

template<typename domainT>
const statet& ait< domainT >::find_state ( locationt  l) const
inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 354 of file ai.h.

◆ fixedpoint()

template<typename domainT>
void ait< domainT >::fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
inlineoverrideprotectedvirtual

Implements ai_baset.

Reimplemented in concurrency_aware_ait< domainT >, and concurrency_aware_ait< rd_range_domaint >.

Definition at line 375 of file ai.h.

◆ get_state()

template<typename domainT>
virtual statet& ait< domainT >::get_state ( locationt  l)
inlineoverrideprotectedvirtual

◆ make_temporary_state()

template<typename domainT>
std::unique_ptr<statet> ait< domainT >::make_temporary_state ( const statet s)
inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 370 of file ai.h.

◆ merge()

template<typename domainT>
bool ait< domainT >::merge ( const statet src,
locationt  from,
locationt  to 
)
inlineoverrideprotectedvirtual

Implements ai_baset.

Definition at line 363 of file ai.h.

Referenced by ait< dep_graph_domaint >::merge().

◆ merge_shared()

template<typename domainT>
bool ait< domainT >::merge_shared ( const statet ,
goto_programt::const_targett  ,
goto_programt::const_targett  ,
const namespacet  
)
inlineoverrideprivatevirtual

Implements ai_baset.

Reimplemented in concurrency_aware_ait< domainT >, and concurrency_aware_ait< rd_range_domaint >.

Definition at line 387 of file ai.h.

◆ operator[]() [1/2]

template<typename domainT>
domainT& ait< domainT >::operator[] ( locationt  l)
inline

Definition at line 304 of file ai.h.

◆ operator[]() [2/2]

template<typename domainT>
const domainT& ait< domainT >::operator[] ( locationt  l) const
inline

Definition at line 313 of file ai.h.

Member Data Documentation

◆ state_map


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