20 traces.push_back(std::move(trace));
23 last_step.is_assert(),
"last goto trace step expected to be assertion");
28 "cannot associate more than one error trace with property " +
31 for(
auto &step :
traces.back().steps)
39 traces.push_back(std::move(trace));
48 for(
auto &step :
traces.back().steps)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const goto_tracet & insert(goto_tracet &&)
Store trace that ends in a violated assertion.
merge_irept merge_ireps
irep container for shared ireps
const namespacet & ns
the namespace related to the traces
const goto_tracet & insert_all(goto_tracet &&)
Store trace that contains multiple violated assertions.
std::unordered_map< irep_idt, std::size_t > property_id_to_trace_index
const goto_tracet & operator[](const irep_idt &property_id) const
const namespacet & get_namespace() const
const std::list< goto_tracet > & all() const
std::list< goto_tracet > traces
stores the traces
goto_trace_storaget(const namespacet &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const std::string & id2string(const irep_idt &d)
#define CHECK_RETURN(CONDITION)
#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'.