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)
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)
168 working = working->
caller;
193 "Implied by if-then-else");
199 else if(this->
caller ==
nullptr)
203 else if(op.
caller ==
nullptr)
227 else if(this->
caller !=
nullptr && op.
caller !=
nullptr)
History for tracking the call stack and performing interprocedural analysis.
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
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
call_stack_entryt(locationt l, cse_ptrt p)
bool operator<(const call_stack_entryt &op) const
bool operator==(const call_stack_entryt &op) const
locationt current_location
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)
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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.