goto_trace_storage.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Trace Storage
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
#define CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H
 
#include <goto-programs/goto_trace.h>
 
#include <util/merge_irep.h>
 
#include <list>
 
class goto_trace_storaget
{
public:
  explicit goto_trace_storaget(const namespacet &);
  goto_trace_storaget(const goto_trace_storaget &) = delete;

  const goto_tracet &insert(goto_tracet &&);

  const goto_tracet &insert_all(goto_tracet &&);
 
  const std::list<goto_tracet> &all() const;
  const goto_tracet &operator[](const irep_idt &property_id) const;
 
  const namespacet &get_namespace() const;
 
protected:
  const namespacet &ns;

  std::list<goto_tracet> traces;
 
  // maps property ID to index in traces
  std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;

  merge_irept merge_ireps;
};
 
#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H