CBMC
Loading...
Searching...
No Matches
goto_trace_storage.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Trace Storage
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
13#define CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
14
16
17#include <util/merge_irep.h>
18
19#include <list>
20
22{
23public:
24 explicit goto_trace_storaget(const namespacet &);
26
29
34
35 const std::list<goto_tracet> &all() const;
36 const goto_tracet &operator[](const irep_idt &property_id) const;
37
38 const namespacet &get_namespace() const;
39
40protected:
42 const namespacet &ns;
43
45 std::list<goto_tracet> traces;
46
47 // maps property ID to index in traces
48 std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;
49
52};
53
54#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.
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
goto_trace_storaget(const goto_trace_storaget &)=delete
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
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
Traces of GOTO Programs.