Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
13 #define CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
31 const std::vector<goto_tracet> &
all()
const;
47 #endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::vector< goto_tracet > traces
stores the traces
std::unordered_map< irep_idt, std::size_t > property_id_to_trace_index
const std::vector< goto_tracet > & all() const
const goto_tracet & operator[](const irep_idt &property_id) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const goto_tracet & insert(goto_tracet &&)
Store trace that ends in a violated assertion.
goto_trace_storaget(const namespacet &)
const goto_tracet & insert_all(goto_tracet &&)
Store trace that contains multiple violated assertions.
const namespacet & get_namespace() const
goto_trace_storaget(const goto_trace_storaget &)=delete
const namespacet & ns
the namespace related to the traces