CBMC
Loading...
Searching...
No Matches
goto_trace_storage.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Trace Storage
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "goto_trace_storage.h"
13
17
19{
20 traces.push_back(std::move(trace));
21 const auto &last_step = traces.back().get_last_step();
23 last_step.is_assert(), "last goto trace step expected to be assertion");
24 const auto emplace_result = property_id_to_trace_index.emplace(
25 last_step.property_id, traces.size() - 1);
27 emplace_result.second,
28 "cannot associate more than one error trace with property " +
29 id2string(last_step.property_id));
30
31 for(auto &step : traces.back().steps)
32 step.merge_ireps(merge_ireps);
33
34 return traces.back();
35}
36
38{
39 traces.push_back(std::move(trace));
40 const auto &all_property_ids = traces.back().get_failed_property_ids();
42 !all_property_ids.empty(), "a trace must violate at least one assertion");
43 for(const auto &property_id : all_property_ids)
44 {
45 property_id_to_trace_index.emplace(property_id, traces.size() - 1);
46 }
47
48 for(auto &step : traces.back().steps)
49 step.merge_ireps(merge_ireps);
50
51 return traces.back();
52}
53
54const std::list<goto_tracet> &goto_trace_storaget::all() const
55{
56 return traces;
57}
58
60operator[](const irep_idt &property_id) const
61{
62 const auto trace_found = property_id_to_trace_index.find(property_id);
64 CHECK_RETURN(trace_found->second < traces.size());
65
66 return *(std::next(traces.begin(), trace_found->second));
67}
68
70{
71 return ns;
72}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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 &)
Trace of a GOTO program.
Definition goto_trace.h:177
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Goto Trace Storage.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423