void output(std::ostream &out) const override
bool operator<(const call_stack_entryt &op) const
static const trace_ptrt no_caller_history
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,...
locationt current_location
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
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.
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...
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.