Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created.
More...
|
bool | is_path_merge_history (void) const |
|
bool | has_histories_per_location_limit (void) const |
|
| local_control_flow_historyt (locationt loc) |
|
| local_control_flow_historyt (locationt loc, lcfd_ptrt hist, size_t max_hist) |
|
| local_control_flow_historyt (locationt loc, size_t max_hist) |
|
| local_control_flow_historyt (const local_control_flow_historyt< track_forward_jumps, track_backward_jumps > &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.
|
|
bool | operator< (const ai_history_baset &op) const override |
| The order for history_sett.
|
|
bool | operator== (const ai_history_baset &op) const override |
| History objects should be comparable.
|
|
const locationt & | current_location (void) const override |
| The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
|
|
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.
|
|
void | output (std::ostream &out) const override |
|
virtual | ~ai_history_baset () |
|
virtual step_returnt | step (locationt to, const trace_sett &others, trace_ptrt caller_hist) const =0 |
| 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.
|
|
virtual bool | operator< (const ai_history_baset &op) const =0 |
| The order for history_sett.
|
|
virtual bool | operator== (const ai_history_baset &op) const =0 |
| History objects should be comparable.
|
|
virtual const locationt & | current_location (void) const =0 |
| The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
|
|
virtual bool | should_widen (const ai_history_baset &other) const |
| 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.
|
|
virtual void | output (std::ostream &out) const |
|
virtual jsont | output_json (void) const |
|
virtual xmlt | output_xml (void) const |
|
template<bool track_forward_jumps, bool track_backward_jumps>
class local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created.
Definition at line 45 of file local_control_flow_history.h.
template<bool track_forward_jumps, bool track_backward_jumps>
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 135 of file local_control_flow_history.h.
template<bool track_forward_jumps, bool track_backward_jumps>
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 16 of file local_control_flow_history.cpp.