#include <ai_storage.h>
Inheritance diagram for history_sensitive_storaget: Collaboration diagram for history_sensitive_storaget: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 () | |
Detailed Description
Definition at line 227 of file ai_storage.h.
Member Typedef Documentation
◆ domain_mapt
|
protected |
Definition at line 231 of file ai_storage.h.
Member Function Documentation
◆ abstract_state_before() [1/2]
|
inlineoverridevirtual |
Implements ai_storage_baset.
Definition at line 246 of file ai_storage.h.
◆ abstract_state_before() [2/2]
|
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.
◆ clear()
|
inlineoverridevirtual |
Reset the abstract state.
Reimplemented from trace_map_storaget.
Definition at line 296 of file ai_storage.h.
◆ get_state()
|
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.
Member Data Documentation
◆ domain_map
|
protected |
Definition at line 232 of file ai_storage.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/analyses/ai_storage.h
