cprover
|
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>
Public Member Functions | |
ahistoricalt (locationt l) | |
ahistoricalt (const ahistoricalt &old) | |
step_returnt | step (locationt to, const trace_sett &others) 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 |
![]() | |
virtual | ~ai_history_baset () |
virtual jsont | output_json (void) const |
virtual xmlt | output_xml (void) const |
Protected Attributes | |
locationt | current |
Additional Inherited Members | |
![]() | |
enum | step_statust { step_statust::NEW, step_statust::MERGED, step_statust::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 |
![]() | |
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 &) | |
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 144 of file ai_history.h.
|
inlineexplicit |
Definition at line 151 of file ai_history.h.
|
inline |
Definition at line 155 of file ai_history.h.
|
inlineoverridevirtual |
The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
Implements ai_history_baset.
Definition at line 203 of file ai_history.h.
|
inlineoverridevirtual |
The order for history_sett.
Implements ai_history_baset.
Definition at line 182 of file ai_history.h.
|
inlineoverridevirtual |
History objects should be comparable.
Implements ai_history_baset.
Definition at line 190 of file ai_history.h.
|
inlineoverridevirtual |
Reimplemented from ai_history_baset.
Definition at line 216 of file ai_history.h.
|
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 211 of file ai_history.h.
|
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.
PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function());
Step may do one of three things :
Implements ai_history_baset.
Definition at line 160 of file ai_history.h.
|
protected |
Definition at line 148 of file ai_history.h.