The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++... More...
#include <ai_history.h>
Inheritance diagram for ahistoricalt: Collaboration diagram for ahistoricalt:Public Member Functions | |
| ahistoricalt (locationt l) | |
| ahistoricalt (const ahistoricalt &old) | |
| step_returnt | step (locationt to, const trace_sett &others, trace_ptrt caller_hist) const override |
| Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point. More... | |
| bool | operator< (const ai_history_baset &op) const override |
| The order for history_sett. More... | |
| bool | operator== (const ai_history_baset &op) const override |
| History objects should be comparable. More... | |
| const locationt & | current_location (void) const override |
| The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable) More... | |
| bool | should_widen (const ai_history_baset &other) const override |
| Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way. More... | |
| void | output (std::ostream &out) const override |
| Public Member Functions inherited from ai_history_baset | |
| virtual | ~ai_history_baset () |
| virtual jsont | output_json (void) const |
| virtual xmlt | output_xml (void) const |
Protected Attributes | |
| locationt | current |
Additional Inherited Members | |
| Public Types inherited from ai_history_baset | |
| enum class | step_statust { NEW , MERGED , BLOCKED } |
| typedef goto_programt::const_targett | locationt |
| typedef std::shared_ptr< const ai_history_baset > | trace_ptrt |
| History objects are intended to be immutable so they can be shared to reduce memory overhead. More... | |
| typedef std::set< trace_ptrt, compare_historyt > | trace_sett |
| typedef std::pair< step_statust, trace_ptrt > | step_returnt |
| Static Public Attributes inherited from ai_history_baset | |
| static const trace_ptrt | no_caller_history |
| Protected Member Functions inherited from ai_history_baset | |
| ai_history_baset (locationt) | |
| Create a new history starting from a given location This is used to start the analysis from scratch PRECONDITION(l.is_dereferenceable());. More... | |
| ai_history_baset (const ai_history_baset &) | |
Detailed Description
The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++...
Definition at line 154 of file ai_history.h.
Constructor & Destructor Documentation
◆ ahistoricalt() [1/2]
|
inlineexplicit |
Definition at line 161 of file ai_history.h.
◆ ahistoricalt() [2/2]
|
inline |
Definition at line 165 of file ai_history.h.
Member Function Documentation
◆ current_location()
|
inlineoverridevirtual |
The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
Implements ai_history_baset.
Definition at line 216 of file ai_history.h.
◆ operator<()
|
inlineoverridevirtual |
The order for history_sett.
Implements ai_history_baset.
Definition at line 195 of file ai_history.h.
◆ operator==()
|
inlineoverridevirtual |
History objects should be comparable.
Implements ai_history_baset.
Definition at line 203 of file ai_history.h.
◆ output()
|
inlineoverridevirtual |
Reimplemented from ai_history_baset.
Definition at line 229 of file ai_history.h.
◆ should_widen()
|
inlineoverridevirtual |
Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way.
However it could be used in other ways (such as the transformer). The key idea is that the history tracks / should know when to widen and when to continue.
Reimplemented from ai_history_baset.
Definition at line 224 of file ai_history.h.
◆ step()
|
inlineoverridevirtual |
Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point.
In the case of function call return it is also given the full history of the caller. This allows function-local histories as they can "pick up" the state from before the call when computing the return edge.
PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function()); PRECONDITION(caller_hist == no_caller_history || current_location()->is_end_function);
Step may do one of three things :
- Create a new history object and return a pointer to it This will force the analyser to continue regardless of domain changes POSTCONDITION(IMPLIES(result.first == step_statust::NEW, result.second.use_count() == 1 ));
- Merge with an existing history This means the analyser will only continue if the domain is updated POSTCONDITION(IMPLIES(result.first == step_statust::MERGED, result.second is an element of others));
- Block this flow of execution This indicates the transition is impossible (returning to a location other than the call location) or undesireable (omitting some traces) POSTCONDITION(IMPLIES(result.first == BLOCKED, result.second == nullptr()));
Implements ai_history_baset.
Definition at line 170 of file ai_history.h.
Member Data Documentation
◆ current
|
protected |
Definition at line 158 of file ai_history.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/analyses/ai_history.h
