Skip to content

Commit 6ad4039

Browse files
Extend goto trace storage to coverage traces
Coverage traces cover several properties.
1 parent 9f55401 commit 6ad4039

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed

src/goto-checker/goto_trace_storage.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,16 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
2525
return traces.back();
2626
}
2727

28+
const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
29+
{
30+
traces.push_back(std::move(trace));
31+
for(const auto &property_id : traces.back().get_all_property_ids())
32+
{
33+
property_id_to_trace_index.emplace(property_id, traces.size() - 1);
34+
}
35+
return traces.back();
36+
}
37+
2838
const std::vector<goto_tracet> &goto_trace_storaget::all() const
2939
{
3040
return traces;

src/goto-checker/goto_trace_storage.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,9 @@ class goto_trace_storaget
2323
/// Store trace that ends in a violated assertion
2424
const goto_tracet &insert(goto_tracet &&);
2525

26+
/// Store trace that contains multiple violated assertions
27+
const goto_tracet &insert_all(goto_tracet &&);
28+
2629
const std::vector<goto_tracet> &all() const;
2730
const goto_tracet &operator[](const irep_idt &property_id) const;
2831

0 commit comments

Comments
 (0)