cprover
history_sensitive_storaget Class Reference

#include <ai_storage.h>

+ Inheritance diagram for history_sensitive_storaget:
+ Collaboration diagram for history_sensitive_storaget:

Public Member Functions

cstate_ptrt abstract_state_before (trace_ptrt p, const ai_domain_factory_baset &fac) const override
 Non-modifying access to the stored domains, used in the ai_baset public interface. More...
 
cstate_ptrt abstract_state_before (locationt t, const ai_domain_factory_baset &fac) const override
 
statetget_state (trace_ptrt p, const ai_domain_factory_baset &fac) override
 Look up the analysis state for a given history, instantiating a new domain if required. More...
 
void clear () override
 Reset the abstract state. More...
 
- Public Member Functions inherited from trace_map_storaget
ctrace_set_ptrt abstract_traces_before (locationt l) const override
 Returns all of the histories that have reached the start of the instruction. More...
 
void clear () override
 Reset the abstract state. More...
 
- Public Member Functions inherited from ai_storage_baset
virtual ~ai_storage_baset ()
 
virtual ctrace_set_ptrt abstract_traces_before (locationt l) const =0
 Returns all of the histories that have reached the start of the instruction. More...
 
virtual cstate_ptrt abstract_state_before (trace_ptrt p, const ai_domain_factory_baset &fac) const =0
 Non-modifying access to the stored domains, used in the ai_baset public interface. More...
 
virtual cstate_ptrt abstract_state_before (locationt l, const ai_domain_factory_baset &fac) const =0
 
virtual statetget_state (trace_ptrt p, const ai_domain_factory_baset &fac)=0
 Look up the analysis state for a given history, instantiating a new domain if required. More...
 
virtual void clear ()
 Reset the abstract state. More...
 
virtual void prune (locationt l)
 Notifies the storage that the user will not need the domain object(s) for this location. More...
 

Protected Types

typedef std::map< trace_ptrt, state_ptrt, ai_history_baset::compare_historytdomain_mapt
 
- Protected Types inherited from trace_map_storaget
typedef std::map< locationt, trace_set_ptrttrace_mapt
 

Protected Attributes

domain_mapt domain_map
 
- Protected Attributes inherited from trace_map_storaget
trace_mapt trace_map
 

Additional Inherited Members

- Public Types inherited from ai_storage_baset
typedef ai_domain_baset statet
 
typedef std::shared_ptr< statetstate_ptrt
 
typedef std::shared_ptr< const statetcstate_ptrt
 
typedef ai_history_baset tracet
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 
typedef ai_history_baset::trace_sett trace_sett
 
typedef std::shared_ptr< trace_setttrace_set_ptrt
 
typedef std::shared_ptr< const trace_settctrace_set_ptrt
 
typedef goto_programt::const_targett locationt
 
- Protected Member Functions inherited from trace_map_storaget
void register_trace (trace_ptrt p)
 
- Protected Member Functions inherited from ai_storage_baset
 ai_storage_baset ()
 

Detailed Description

Definition at line 226 of file ai_storage.h.

Member Typedef Documentation

◆ domain_mapt

Member Function Documentation

◆ abstract_state_before() [1/2]

cstate_ptrt history_sensitive_storaget::abstract_state_before ( locationt  t,
const ai_domain_factory_baset fac 
) const
inlineoverridevirtual

Implements ai_storage_baset.

Definition at line 245 of file ai_storage.h.

◆ abstract_state_before() [2/2]

cstate_ptrt history_sensitive_storaget::abstract_state_before ( trace_ptrt  p,
const ai_domain_factory_baset fac 
) const
inlineoverridevirtual

Non-modifying access to the stored domains, used in the ai_baset public interface.

In the case of un-analysed locals this should create a domain The history version is the primary version, the location one may simply join all of the histories that reach the given location

Implements ai_storage_baset.

Definition at line 234 of file ai_storage.h.

◆ clear()

void history_sensitive_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from trace_map_storaget.

Definition at line 295 of file ai_storage.h.

◆ get_state()

statet & history_sensitive_storaget::get_state ( trace_ptrt  p,
const ai_domain_factory_baset fac 
)
inlineoverridevirtual

Look up the analysis state for a given history, instantiating a new domain if required.

Implements ai_storage_baset.

Definition at line 279 of file ai_storage.h.

Member Data Documentation

◆ domain_map

domain_mapt history_sensitive_storaget::domain_map
protected

Definition at line 231 of file ai_storage.h.


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