cprover
location_sensitive_storaget Class Reference

The most conventional storage; one domain per location. More...

#include <ai_storage.h>

+ Inheritance diagram for location_sensitive_storaget:
+ Collaboration diagram for location_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 l, 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...
 
statetget_state (locationt l, const ai_domain_factory_baset &fac)
 
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::unordered_map< locationt, state_ptrt, const_target_hash, pointee_address_equaltstate_mapt
 This is location sensitive so we store one domain per location. More...
 
- Protected Types inherited from trace_map_storaget
typedef std::map< locationt, trace_set_ptrttrace_mapt
 

Protected Member Functions

state_maptinternal (void)
 
- 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 ()
 

Protected Attributes

state_mapt state_map
 
friend invariant_propagationt
 
friend dependence_grapht
 
friend variable_sensitivity_dependence_grapht
 
- 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
 

Detailed Description

The most conventional storage; one domain per location.

Definition at line 152 of file ai_storage.h.

Member Typedef Documentation

◆ state_mapt

This is location sensitive so we store one domain per location.

Definition at line 161 of file ai_storage.h.

Member Function Documentation

◆ abstract_state_before() [1/2]

cstate_ptrt location_sensitive_storaget::abstract_state_before ( locationt  l,
const ai_domain_factory_baset fac 
) const
inlineoverridevirtual

Implements ai_storage_baset.

Definition at line 181 of file ai_storage.h.

◆ abstract_state_before() [2/2]

cstate_ptrt location_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 174 of file ai_storage.h.

◆ clear()

void location_sensitive_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from trace_map_storaget.

Definition at line 217 of file ai_storage.h.

◆ get_state() [1/2]

statet & location_sensitive_storaget::get_state ( locationt  l,
const ai_domain_factory_baset fac 
)
inline
Deprecated:
SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead")

Definition at line 203 of file ai_storage.h.

◆ get_state() [2/2]

statet & location_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 192 of file ai_storage.h.

◆ internal()

state_mapt & location_sensitive_storaget::internal ( void  )
inlineprotected

Definition at line 168 of file ai_storage.h.

Member Data Documentation

◆ dependence_grapht

friend location_sensitive_storaget::dependence_grapht
protected

Definition at line 166 of file ai_storage.h.

◆ invariant_propagationt

friend location_sensitive_storaget::invariant_propagationt
protected

Definition at line 165 of file ai_storage.h.

◆ state_map

state_mapt location_sensitive_storaget::state_map
protected

Definition at line 162 of file ai_storage.h.

◆ variable_sensitivity_dependence_grapht

friend location_sensitive_storaget::variable_sensitivity_dependence_grapht
protected

Definition at line 167 of file ai_storage.h.


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