cprover
Loading...
Searching...
No Matches
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.
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.
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::map< trace_ptrt, state_ptrt, ai_history_baset::compare_historytdomain_mapt
Protected Types inherited from trace_map_storaget
typedef std::map< locationt, trace_set_ptrt, goto_programt::target_less_thantrace_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 227 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 246 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 235 of file ai_storage.h.

◆ clear()

void history_sensitive_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from ai_storage_baset.

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

Member Data Documentation

◆ domain_map

domain_mapt history_sensitive_storaget::domain_map
protected

Definition at line 232 of file ai_storage.h.


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