cprover
trace_map_storaget Class Reference

#include <ai_storage.h>

+ Inheritance diagram for trace_map_storaget:
+ Collaboration diagram for trace_map_storaget:

Public Member Functions

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::map< locationt, trace_set_ptrttrace_mapt
 

Protected Member Functions

void register_trace (trace_ptrt p)
 
- Protected Member Functions inherited from ai_storage_baset
 ai_storage_baset ()
 

Protected Attributes

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

Definition at line 100 of file ai_storage.h.

Member Typedef Documentation

◆ trace_mapt

Definition at line 103 of file ai_storage.h.

Member Function Documentation

◆ abstract_traces_before()

ctrace_set_ptrt trace_map_storaget::abstract_traces_before ( locationt  l) const
inlineoverridevirtual

Returns all of the histories that have reached the start of the instruction.

Implements ai_storage_baset.

Definition at line 127 of file ai_storage.h.

◆ clear()

void trace_map_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from ai_storage_baset.

Reimplemented in location_sensitive_storaget, and history_sensitive_storaget.

Definition at line 138 of file ai_storage.h.

◆ register_trace()

void trace_map_storaget::register_trace ( trace_ptrt  p)
inlineprotected

Definition at line 107 of file ai_storage.h.

Member Data Documentation

◆ trace_map

trace_mapt trace_map_storaget::trace_map
protected

Definition at line 104 of file ai_storage.h.


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