CBMC
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...
 
- 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::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 trace_map_storaget.

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: