Go to the documentation of this file.
16 std::ostringstream out;
19 return std::move(
json);
24 std::ostringstream out;
44 if(l_return->location_number == to->location_number)
48 std::make_shared<call_stack_entryt>(l_return,
current_stack->caller));
61 unsigned int number_of_recursive_calls = 0;
68 i->current_location->location_number ==
72 if(first_found ==
nullptr)
76 ++number_of_recursive_calls;
79 shorten = first_found;
86 next_stack =
cse_ptrt(std::make_shared<call_stack_entryt>(to, shorten));
103 if(l_caller_return->location_number == to->location_number)
106 next_stack =
cse_ptrt(std::make_shared<call_stack_entryt>(
122 INVARIANT(next_stack !=
nullptr,
"All branches should initialise next_stack");
130 auto it = others.find(next);
132 if(it == others.end())
160 out <<
"call_stack_history : stack "
163 while(working !=
nullptr)
165 out <<
" from " << working->current_location->location_number;
166 working = working->caller;
191 "Implied by if-then-else");
197 else if(this->
caller ==
nullptr)
201 else if(op.
caller ==
nullptr)
221 if(this->caller == op.
caller)
225 else if(this->caller !=
nullptr && op.
caller !=
nullptr)
227 return *(this->caller) == *(op.
caller);
#define UNREACHABLE
This should be used to mark dead code.
void output(std::ostream &out) const override
virtual void output(std::ostream &out) const
bool operator<(const call_stack_entryt &op) const
bool has_recursion_limit(void) const
const locationt & current_location(void) const override
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
std::shared_ptr< const call_stack_entryt > cse_ptrt
std::set< trace_ptrt, compare_historyt > trace_sett
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
virtual xmlt output_xml(void) const
#define PRECONDITION(CONDITION)
locationt current_location
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
virtual jsont output_json(void) const
step_returnt step(locationt to, const trace_sett &others) const override
Step creates a new history by advancing the current one to location "to" It is given the set of all o...
goto_programt::const_targett locationt
unsigned int recursion_limit
A history object is an abstraction / representation of the control-flow part of a set of traces.
call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
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.
Records the call stack Care must be taken when using this on recursive code; it will need the domain ...
std::pair< step_statust, trace_ptrt > step_returnt
bool operator==(const call_stack_entryt &op) const
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.