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 <call_stack_history.h>
Inheritance diagram for call_stack_historyt: Collaboration diagram for call_stack_historyt: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, 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 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) | |
| 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 &) | |
Protected Attributes | |
| cse_ptrt | current_stack |
| unsigned int | recursion_limit |
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 |
Detailed Description
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 20 of file call_stack_history.h.
Member Typedef Documentation
◆ cse_ptrt
|
protected |
Definition at line 24 of file call_stack_history.h.
Constructor & Destructor Documentation
◆ call_stack_historyt() [1/4]
|
inlineprotected |
Definition at line 53 of file call_stack_history.h.
◆ call_stack_historyt() [2/4]
|
inlineexplicit |
Definition at line 63 of file call_stack_history.h.
◆ call_stack_historyt() [3/4]
|
inline |
Definition at line 70 of file call_stack_history.h.
◆ call_stack_historyt() [4/4]
|
inline |
Definition at line 77 of file call_stack_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 92 of file call_stack_history.h.
◆ has_recursion_limit()
|
inlineprotected |
Definition at line 48 of file call_stack_history.h.
◆ operator<()
|
overridevirtual |
The order for history_sett.
Implements ai_history_baset.
Definition at line 144 of file call_stack_history.cpp.
◆ operator==()
|
overridevirtual |
History objects should be comparable.
Implements ai_history_baset.
Definition at line 152 of file call_stack_history.cpp.
◆ output()
|
overridevirtual |
Reimplemented from ai_history_baset.
Definition at line 160 of file call_stack_history.cpp.
◆ 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 100 of file call_stack_history.h.
◆ step()
|
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.
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 14 of file call_stack_history.cpp.
Member Data Documentation
◆ current_stack
|
protected |
Definition at line 39 of file call_stack_history.h.
◆ recursion_limit
|
protected |
Definition at line 46 of file call_stack_history.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/call_stack_history.h
- /home/runner/work/cbmc/cbmc/src/analyses/call_stack_history.cpp
