29 if(l_return->location_number == to->location_number)
33 std::make_shared<call_stack_entryt>(l_return,
current_stack->caller));
46 unsigned int number_of_recursive_calls = 0;
53 i->current_location->location_number ==
57 if(first_found ==
nullptr)
61 ++number_of_recursive_calls;
64 shorten = first_found;
71 next_stack =
cse_ptrt(std::make_shared<call_stack_entryt>(to, shorten));
86 "return from function should have a caller");
92 if(l_caller_return->location_number == to->location_number)
95 std::next(caller_hist->current_location())->location_number ==
96 l_caller_return->location_number,
97 "caller and caller_hist should be consistent");
108 next_stack =
cse_ptrt(std::make_shared<call_stack_entryt>(
124 INVARIANT(next_stack !=
nullptr,
"All branches should initialise next_stack");
132 auto it = others.find(next);
134 if(it == others.end())
162 out <<
"call_stack_history : stack "
165 while(working !=
nullptr)
167 out <<
" from " << working->current_location->location_number;
168 working = working->caller;
193 "Implied by if-then-else");
199 else if(this->
caller ==
nullptr)
203 else if(op.
caller ==
nullptr)
223 if(this->caller == op.
caller)
227 else if(this->caller !=
nullptr && op.
caller !=
nullptr)
229 return *(this->caller) == *(op.
caller);
History for tracking the call stack and performing interprocedural analysis.
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
bool operator<(const call_stack_entryt &op) const
bool operator==(const call_stack_entryt &op) const
locationt current_location
Records the call stack Care must be taken when using this on recursive code; it will need the domain ...
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
std::shared_ptr< const call_stack_entryt > cse_ptrt
call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
const locationt & current_location(void) const override
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
void output(std::ostream &out) const override
bool has_recursion_limit(void) const
unsigned int recursion_limit
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
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...
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)