CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
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 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 statet & get_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 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_ptrt, goto_programt::target_less_than > trace_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< statet > state_ptrt
 
typedef std::shared_ptr< const statet > cstate_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_sett > trace_set_ptrt
 
typedef std::shared_ptr< const trace_sett > ctrace_set_ptrt
 
typedef goto_programt::const_targett locationt
 

Detailed Description

Definition at line 100 of file ai_storage.h.

Member Typedef Documentation

◆ trace_mapt

typedef std::map<locationt, trace_set_ptrt, goto_programt::target_less_than> trace_map_storaget::trace_mapt
protected

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

◆ clear()

void trace_map_storaget::clear ( )
inlineoverridevirtual

Reset the abstract state.

Reimplemented from ai_storage_baset.

Reimplemented in history_sensitive_storaget, and location_sensitive_storaget.

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: