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 :

1. 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 ));
2. 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));
3. 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()));

Implemented in ahistoricalt, call_stack_historyt, and local_control_flow_historyt< track_forward_jumps, track_backward_jumps >.