cprover
Loading...
Searching...
No Matches
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.
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.
statetget_state (locationt l, const ai_domain_factory_baset &fac)
void clear () override
 Reset the abstract state.
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.
void clear () override
 Reset the abstract state.
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.

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.
Protected Types inherited from trace_map_storaget
typedef std::map< locationt, trace_set_ptrt, goto_programt::target_less_thantrace_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 153 of file ai_storage.h.

Member Typedef Documentation

◆ state_mapt

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 ai_storage_baset.

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
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: