14template <
bool track_forward_jumps,
bool track_backward_jumps>
26 track_backward_jumps>>
32 (
current_loc->is_backwards_goto() ? track_backward_jumps
33 : track_forward_jumps))
35 bool branch_taken = (
current_loc->get_target() == to) &&
42 auto decision = std::make_shared<local_control_flow_decisiont>(
44 next_step = std::make_shared<
50 std::next(this->current_loc)->location_number != to->location_number)
55 if(others.size() == 0)
57 next_step = std::make_shared<
66 "Function start should have at most one merged history");
69 ->is_path_merge_history(),
70 "The one history must be a merge point");
72 return std::make_pair(
82 next_step = std::make_shared<
92 next_step = std::make_shared<
97 next_step !=
nullptr,
"All branches should create a candidate history");
100 auto it = others.find(next_step);
101 if(it == others.end())
105 auto number_of_histories = others.size();
125 auto last_history_pointer = std::prev(others.end());
130 "The last history must be the merged one");
132 return std::make_pair(
139 "Histories-per-location limit should be enforced");
156template <
bool track_forward_jumps,
bool track_backward_jumps>
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)
180 other.control_flow_decision_history)
185 else if(other.control_flow_decision_history ==
nullptr)
201 *(other.control_flow_decision_history));
207template <
bool track_forward_jumps,
bool track_backward_jumps>
211 auto other =
dynamic_cast<
216 if(this->
current_loc->location_number == other.current_loc->location_number)
220 other.control_flow_decision_history)
226 other.control_flow_decision_history ==
nullptr)
238 *(other.control_flow_decision_history));
248template <
bool track_forward_jumps,
bool track_backward_jumps>
250 output(std::ostream &out)
const
252 out <<
"local_control_flow_history : location "
255 while(working !=
nullptr)
292 "Implied by if-then-else");
363 const trace_sett &others,
364 trace_ptrt caller_hist)
const;
369 const trace_sett &others,
370 trace_ptrt caller_hist)
const;
375 const trace_sett &others,
376 trace_ptrt caller_hist)
const;
381 const trace_sett &others,
382 trace_ptrt caller_hist)
const;
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
ai_history_baset(locationt)
Create a new history starting from a given location This is used to start the analysis from scratch P...
goto_programt::const_targett locationt
std::set< trace_ptrt, compare_historyt > trace_sett
local_control_flow_decisiont(locationt loc, bool taken, lcfd_ptrt ptr)
bool operator<(const local_control_flow_decisiont &op) const
bool operator==(const local_control_flow_decisiont &op) const
locationt branch_location
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
local_control_flow_historyt(locationt loc)
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
bool has_histories_per_location_limit(void) const
std::shared_ptr< const local_control_flow_historyt< track_forward_jumps, track_backward_jumps > > to_local_control_flow_history(trace_ptrt in) const
lcfd_ptrt control_flow_decision_history
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...
size_t max_histories_per_location
bool is_path_merge_history(void) const
Track function-local control flow for loop unwinding and path senstivity.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.