26 track_backward_jumps>>
31 current_loc->is_goto() &&
32 (current_loc->is_backwards_goto() ? track_backward_jumps
33 : track_forward_jumps))
35 bool branch_taken = (current_loc->get_target() ==
to) &&
36 !(current_loc->get_target() == std::next(current_loc));
42 auto decision = std::make_shared<local_control_flow_decisiont>(
43 current_loc, branch_taken, control_flow_decision_history);
49 current_loc->is_function_call() &&
50 std::next(this->current_loc)->location_number !=
to->location_number)
59 to,
nullptr, max_histories_per_location);
66 "Function start should have at most one merged history");
68 to_local_control_flow_history(*(
others.begin()))
69 ->is_path_merge_history(),
70 "The one history must be a merge point");
72 return std::make_pair(
76 else if(current_loc->is_end_function())
85 to_local_control_flow_history(
caller_hist)->control_flow_decision_history,
86 max_histories_per_location);
94 to, control_flow_decision_history, max_histories_per_location);
97 next_step !=
nullptr,
"All branches should create a candidate history");
103 if(has_histories_per_location_limit())
117 track_backward_jumps>>(
to,
nullptr, max_histories_per_location);
120 else if(
others.size() == max_histories_per_location)
129 ->is_path_merge_history(),
130 "The last history must be the merged one");
132 return std::make_pair(
138 others.size() <= max_histories_per_location,
139 "Histories-per-location limit should be enforced");
160 auto other =
dynamic_cast<
167 if(this->current_loc->location_number < other.current_loc->location_number)
172 this->current_loc->location_number > other.current_loc->location_number)
179 this->control_flow_decision_history ==
180 other.control_flow_decision_history)
185 else if(other.control_flow_decision_history ==
nullptr)
192 else if(this->control_flow_decision_history ==
nullptr)
200 *(this->control_flow_decision_history) <
201 *(other.control_flow_decision_history));
211 auto other =
dynamic_cast<
216 if(this->current_loc->location_number == other.current_loc->location_number)
219 this->control_flow_decision_history ==
220 other.control_flow_decision_history)
225 this->control_flow_decision_history ==
nullptr ||
226 other.control_flow_decision_history ==
nullptr)
237 *(this->control_flow_decision_history) ==
238 *(other.control_flow_decision_history));
A history object is an abstraction / representation of the control-flow part of a set of traces.
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.
std::pair< step_statust, trace_ptrt > step_returnt
static const trace_ptrt no_caller_history
goto_programt::const_targett locationt
std::set< trace_ptrt, compare_historyt > trace_sett
Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be va...
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
void output(std::ostream &out) const override
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
local_control_flow_decisiont::lcfd_ptrt lcfd_ptrt
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 o...
Track function-local control flow for loop unwinding and path senstivity.