CBMC
|
#include <ai_storage.h>
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 |
statet & | get_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_historyt > | domain_mapt |
Protected Types inherited from trace_map_storaget | |
typedef std::map< locationt, trace_set_ptrt, goto_programt::target_less_than > | trace_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< 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 |
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 () | |
Definition at line 227 of file ai_storage.h.
|
protected |
Definition at line 231 of file ai_storage.h.
|
inlineoverridevirtual |
Implements ai_storage_baset.
Definition at line 246 of file ai_storage.h.
|
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.
|
inlineoverridevirtual |
Reset the abstract state.
Reimplemented from trace_map_storaget.
Definition at line 296 of file ai_storage.h.
|
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.
|
protected |
Definition at line 232 of file ai_storage.h.