cprover
goto_trace_storage.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Trace Storage
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_trace_storage.h"
13 
15 {
16 }
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);
26  INVARIANT(
27  emplace_result.second,
28  "cannot associate more than one error trace with property " +
29  id2string(last_step.property_id));
30  return traces.back();
31 }
32 
34 {
35  traces.push_back(std::move(trace));
36  const auto &all_property_ids = traces.back().get_failed_property_ids();
38  !all_property_ids.empty(), "a trace must violate at least one assertion");
39  for(const auto &property_id : all_property_ids)
40  {
41  property_id_to_trace_index.emplace(property_id, traces.size() - 1);
42  }
43  return traces.back();
44 }
45 
46 const std::vector<goto_tracet> &goto_trace_storaget::all() const
47 {
48  return traces;
49 }
50 
52 operator[](const irep_idt &property_id) const
53 {
54  const auto trace_found = property_id_to_trace_index.find(property_id);
55  PRECONDITION(trace_found != property_id_to_trace_index.end());
56 
57  return traces.at(trace_found->second);
58 }
59 
61 {
62  return ns;
63 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_trace_storaget::traces
std::vector< goto_tracet > traces
stores the traces
Definition: goto_trace_storage.h:41
goto_trace_storaget::property_id_to_trace_index
std::unordered_map< irep_idt, std::size_t > property_id_to_trace_index
Definition: goto_trace_storage.h:44
goto_trace_storaget::all
const std::vector< goto_tracet > & all() const
Definition: goto_trace_storage.cpp:46
goto_trace_storaget::operator[]
const goto_tracet & operator[](const irep_idt &property_id) const
Definition: goto_trace_storage.cpp:52
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_trace_storaget::insert
const goto_tracet & insert(goto_tracet &&)
Store trace that ends in a violated assertion.
Definition: goto_trace_storage.cpp:18
goto_trace_storage.h
Goto Trace Storage.
goto_trace_storaget::goto_trace_storaget
goto_trace_storaget(const namespacet &)
Definition: goto_trace_storage.cpp:14
goto_trace_storaget::insert_all
const goto_tracet & insert_all(goto_tracet &&)
Store trace that contains multiple violated assertions.
Definition: goto_trace_storage.cpp:33
goto_trace_storaget::get_namespace
const namespacet & get_namespace() const
Definition: goto_trace_storage.cpp:60
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
goto_trace_storaget::ns
const namespacet & ns
the namespace related to the traces
Definition: goto_trace_storage.h:38
validation_modet::INVARIANT
@ INVARIANT