CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
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
 
statet & get_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...
 
statet & get_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...
 
- Public Member Functions inherited from ai_storage_baset
virtual ~ai_storage_baset ()
 
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_equalt > state_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_ptrt, goto_programt::target_less_than > trace_mapt
 

Protected Member Functions

state_mapt & internal (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< statet > state_ptrt
 
typedef std::shared_ptr< const statet > cstate_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_sett > trace_set_ptrt
 
typedef std::shared_ptr< const trace_sett > ctrace_set_ptrt
 
typedef goto_programt::const_targett locationt
 

Detailed Description

The most conventional storage; one domain per location.

Definition at line 153 of file ai_storage.h.

Member Typedef Documentation

◆ state_mapt

typedef std::unordered_map< locationt, state_ptrt, const_target_hash, pointee_address_equalt> location_sensitive_storaget::state_mapt
protected

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

Definition at line 162 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 182 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 175 of file ai_storage.h.

◆ clear()

void location_sensitive_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from trace_map_storaget.

Definition at line 218 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:
"deprecated since " "2019" "-" "08" "-" "01" "; " "use get_state(trace_ptrt p) instead"

Definition at line 204 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 193 of file ai_storage.h.

◆ internal()

state_mapt& location_sensitive_storaget::internal ( void  )
inlineprotected

Definition at line 169 of file ai_storage.h.

Member Data Documentation

◆ dependence_grapht

friend location_sensitive_storaget::dependence_grapht
protected

Definition at line 167 of file ai_storage.h.

◆ invariant_propagationt

friend location_sensitive_storaget::invariant_propagationt
protected

Definition at line 166 of file ai_storage.h.

◆ state_map

state_mapt location_sensitive_storaget::state_map
protected

Definition at line 163 of file ai_storage.h.

◆ variable_sensitivity_dependence_grapht

friend location_sensitive_storaget::variable_sensitivity_dependence_grapht
protected

Definition at line 168 of file ai_storage.h.

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