cprover
Loading...
Searching...
No Matches
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.
void clear () override
 Reset the abstract state.
Public Member Functions inherited from ai_storage_baset
virtual ~ai_storage_baset ()
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.
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.
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< locationt, trace_set_ptrt, goto_programt::target_less_thantrace_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

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 128 of file ai_storage.h.

◆ clear()

void trace_map_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from ai_storage_baset.

Definition at line 139 of file ai_storage.h.

◆ register_trace()

void trace_map_storaget::register_trace ( trace_ptrt p)
inlineprotected

Definition at line 108 of file ai_storage.h.

Member Data Documentation

◆ trace_map

trace_mapt trace_map_storaget::trace_map
protected

Definition at line 105 of file ai_storage.h.


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