cprover
goto_trace_storage.h
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 #ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
13 #define CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
14 
16 
18 {
19 public:
20  explicit goto_trace_storaget(const namespacet &);
22 
24  const goto_tracet &insert(goto_tracet &&);
25 
30 
31  const std::vector<goto_tracet> &all() const;
32  const goto_tracet &operator[](const irep_idt &property_id) const;
33 
34  const namespacet &get_namespace() const;
35 
36 protected:
38  const namespacet &ns;
39 
41  std::vector<goto_tracet> traces;
42 
43  // maps property ID to index in traces
44  std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;
45 };
46 
47 #endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
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.h
Traces of GOTO Programs.
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
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_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
Definition: goto_trace_storage.h:18
goto_trace_storaget::get_namespace
const namespacet & get_namespace() const
Definition: goto_trace_storage.cpp:60
goto_trace_storaget::goto_trace_storaget
goto_trace_storaget(const goto_trace_storaget &)=delete
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