cprover
|
Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion. More...
#include <ai_history.h>
Classes | |
class | call_stack_entryt |
Public Member Functions | |
call_stack_historyt (locationt l) | |
call_stack_historyt (locationt l, unsigned int rec_lim) | |
call_stack_historyt (const call_stack_historyt &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 Types | |
typedef std::shared_ptr< const call_stack_entryt > | cse_ptrt |
Protected Member Functions | |
bool | has_recursion_limit (void) const |
call_stack_historyt (cse_ptrt cur_stack, unsigned int rec_lim) | |
![]() | |
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 &) | |
Protected Attributes | |
cse_ptrt | current_stack |
unsigned int | recursion_limit |
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 |
Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion.
Definition at line 225 of file ai_history.h.
|
protected |
Definition at line 229 of file ai_history.h.
|
inlineprotected |
Definition at line 258 of file ai_history.h.
|
inlineexplicit |
Definition at line 268 of file ai_history.h.
|
inline |
Definition at line 275 of file ai_history.h.
|
inline |
Definition at line 282 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 294 of file ai_history.h.
|
inlineprotected |
Definition at line 253 of file ai_history.h.
|
overridevirtual |
The order for history_sett.
Implements ai_history_baset.
Definition at line 142 of file ai_history.cpp.
|
overridevirtual |
History objects should be comparable.
Implements ai_history_baset.
Definition at line 150 of file ai_history.cpp.
|
overridevirtual |
Reimplemented from ai_history_baset.
Definition at line 158 of file ai_history.cpp.
|
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 302 of file ai_history.h.
|
overridevirtual |
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 32 of file ai_history.cpp.
|
protected |
Definition at line 244 of file ai_history.h.
|
protected |
Definition at line 251 of file ai_history.h.