CBMC
Public Types | Public Member Functions | Protected Member Functions | List of all members
ai_storage_baset Class Referenceabstract

This is the basic interface for storing domains. More...

#include <ai_storage.h>

+ Inheritance diagram for ai_storage_baset:

Public Types

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
 

Public Member Functions

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 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 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 Member Functions

 ai_storage_baset ()
 

Detailed Description

This is the basic interface for storing domains.

The abstract interpreters should use this interface by default.

Definition at line 35 of file ai_storage.h.

Member Typedef Documentation

◆ cstate_ptrt

typedef std::shared_ptr<const statet> ai_storage_baset::cstate_ptrt

Definition at line 49 of file ai_storage.h.

◆ ctrace_set_ptrt

typedef std::shared_ptr<const trace_sett> ai_storage_baset::ctrace_set_ptrt

Definition at line 54 of file ai_storage.h.

◆ locationt

typedef goto_programt::const_targett ai_storage_baset::locationt

Definition at line 55 of file ai_storage.h.

◆ state_ptrt

typedef std::shared_ptr<statet> ai_storage_baset::state_ptrt

Definition at line 48 of file ai_storage.h.

◆ statet

typedef ai_domain_baset ai_storage_baset::statet

Definition at line 47 of file ai_storage.h.

◆ trace_ptrt

typedef ai_history_baset::trace_ptrt ai_storage_baset::trace_ptrt

Definition at line 51 of file ai_storage.h.

◆ trace_set_ptrt

typedef std::shared_ptr<trace_sett> ai_storage_baset::trace_set_ptrt

Definition at line 53 of file ai_storage.h.

◆ trace_sett

typedef ai_history_baset::trace_sett ai_storage_baset::trace_sett

Definition at line 52 of file ai_storage.h.

◆ tracet

typedef ai_history_baset ai_storage_baset::tracet

Definition at line 50 of file ai_storage.h.

Constructor & Destructor Documentation

◆ ai_storage_baset()

ai_storage_baset::ai_storage_baset ( )
inlineprotected

Definition at line 38 of file ai_storage.h.

◆ ~ai_storage_baset()

virtual ai_storage_baset::~ai_storage_baset ( )
inlinevirtual

Definition at line 43 of file ai_storage.h.

Member Function Documentation

◆ abstract_state_before() [1/2]

virtual cstate_ptrt ai_storage_baset::abstract_state_before ( locationt  l,
const ai_domain_factory_baset &  fac 
) const
pure virtual

Implemented in history_sensitive_storaget, and location_sensitive_storaget.

◆ abstract_state_before() [2/2]

virtual cstate_ptrt ai_storage_baset::abstract_state_before ( trace_ptrt  p,
const ai_domain_factory_baset &  fac 
) const
pure virtual

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

Implemented in history_sensitive_storaget, and location_sensitive_storaget.

◆ abstract_traces_before()

virtual ctrace_set_ptrt ai_storage_baset::abstract_traces_before ( locationt  l) const
pure virtual

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

Implemented in trace_map_storaget.

◆ clear()

virtual void ai_storage_baset::clear ( )
inlinevirtual

Reset the abstract state.

Reimplemented in history_sensitive_storaget, location_sensitive_storaget, and trace_map_storaget.

Definition at line 80 of file ai_storage.h.

◆ get_state()

virtual statet& ai_storage_baset::get_state ( trace_ptrt  p,
const ai_domain_factory_baset &  fac 
)
pure virtual

Look up the analysis state for a given history, instantiating a new domain if required.

Implemented in history_sensitive_storaget, and location_sensitive_storaget.

◆ prune()

virtual void ai_storage_baset::prune ( locationt  l)
inlinevirtual

Notifies the storage that the user will not need the domain object(s) for this location.

After this has been called abstract_state_before may return an over-approximation of the value and get_state may give an under-approximation (forcing recomputation). If there are multiple histories that reach this location all will be affected

Definition at line 91 of file ai_storage.h.

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