Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_AI_HISTORY_H
13 #define CPROVER_ANALYSES_AI_HISTORY_H
43 typedef std::shared_ptr<const ai_history_baset>
trace_ptrt;
79 typedef std::set<trace_ptrt, compare_historyt>
trace_sett;
134 virtual void output(std::ostream &out)
const
171 INVARIANT(others.size() == 1,
"Only needs one history per location");
173 const auto it = others.begin();
176 "The next location in history map must contain next history");
216 void output(std::ostream &out)
const override
229 typedef std::shared_ptr<const call_stack_entryt>
cse_ptrt;
264 cur_stack !=
nullptr);
307 void output(std::ostream &out)
const override;
327 template <
typename traceT>
362 #endif // CPROVER_ANALYSES_AI_HISTORY_H
void output(std::ostream &out) const override
call_stack_entryt(locationt l, cse_ptrt p)
virtual bool operator==(const ai_history_baset &op) const =0
History objects should be comparable.
virtual void output(std::ostream &out) const
The common case of history is to only care about where you are now, not how you got there!...
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
unsigned int recursion_limit
call_stack_historyt(locationt l, unsigned int rec_lim)
virtual ~ai_history_baset()
In a number of places we need to work with sets of histories so that these (a) make use of the immuta...
bool operator<(const call_stack_entryt &op) const
virtual step_returnt step(locationt to, const trace_sett &others) const =0
Step creates a new history by advancing the current one to location "to" It is given the set of all o...
bool should_widen(const ai_history_baset &other) const override
Domains with a substantial height may need to widen when merging this method allows the history to pr...
virtual ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt)=0
Creates a new history from the given starting point.
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
bool has_recursion_limit(void) const
ai_history_baset(const ai_history_baset &)
virtual bool operator<(const ai_history_baset &op) const =0
The order for history_sett.
ahistoricalt(locationt l)
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
virtual xmlt output_xml(void) const
ahistoricalt(const ahistoricalt &old)
An easy factory implementation for histories that don't need parameters.
call_stack_historyt(const call_stack_historyt &old)
#define PRECONDITION(CONDITION)
locationt current_location
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
bool should_widen(const ai_history_baset &other) const override
Domains with a substantial height may need to widen when merging this method allows the history to pr...
virtual jsont output_json(void) const
void output(std::ostream &out) const override
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
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...
virtual ~ai_history_factory_baset()
unsigned int recursion_limit
virtual ~call_stack_history_factoryt()
call_stack_historyt(locationt l)
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)
ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
Creates a new history from the given starting point.
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.
ai_history_baset(locationt)
Create a new history starting from a given location This is used to start the analysis from scratch P...
As more detailed histories can get complex (for example, nested loops or deep, mutually recursive cal...
Records the call stack Care must be taken when using this on recursive code; it will need the domain ...
bool operator()(const trace_ptrt &l, const trace_ptrt &r) const
std::pair< step_statust, trace_ptrt > step_returnt
instructionst::const_iterator const_targett
const locationt & current_location(void) const override
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
virtual bool should_widen(const ai_history_baset &other) const
Domains with a substantial height may need to widen when merging this method allows the history to pr...
call_stack_history_factoryt(unsigned int rec_lim)
ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
Creates a new history from the given starting point.
bool operator==(const call_stack_entryt &op) const
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.