cprover
goto_trace_storaget Class Reference

#include <goto_trace_storage.h>

+ Collaboration diagram for goto_trace_storaget:

Public Member Functions

 goto_trace_storaget (const namespacet &)
 
 goto_trace_storaget (const goto_trace_storaget &)=delete
 
const goto_tracetinsert (goto_tracet &&)
 Store trace that ends in a violated assertion. More...
 
const goto_tracetinsert_all (goto_tracet &&)
 Store trace that contains multiple violated assertions. More...
 
const std::vector< goto_tracet > & all () const
 
const goto_tracetoperator[] (const irep_idt &property_id) const
 
const namespacetget_namespace () const
 

Protected Attributes

const namespacetns
 the namespace related to the traces More...
 
std::vector< goto_tracettraces
 stores the traces More...
 
std::unordered_map< irep_idt, std::size_t > property_id_to_trace_index
 

Detailed Description

Definition at line 17 of file goto_trace_storage.h.

Constructor & Destructor Documentation

◆ goto_trace_storaget() [1/2]

goto_trace_storaget::goto_trace_storaget ( const namespacet ns)
explicit

Definition at line 14 of file goto_trace_storage.cpp.

◆ goto_trace_storaget() [2/2]

goto_trace_storaget::goto_trace_storaget ( const goto_trace_storaget )
delete

Member Function Documentation

◆ all()

const std::vector< goto_tracet > & goto_trace_storaget::all ( ) const

Definition at line 46 of file goto_trace_storage.cpp.

◆ get_namespace()

const namespacet & goto_trace_storaget::get_namespace ( ) const

Definition at line 60 of file goto_trace_storage.cpp.

◆ insert()

const goto_tracet & goto_trace_storaget::insert ( goto_tracet &&  trace)

Store trace that ends in a violated assertion.

Definition at line 18 of file goto_trace_storage.cpp.

◆ insert_all()

const goto_tracet & goto_trace_storaget::insert_all ( goto_tracet &&  trace)

Store trace that contains multiple violated assertions.

Note
Only property IDs that are not part of any already stored trace are mapped to the given trace.

Definition at line 33 of file goto_trace_storage.cpp.

◆ operator[]()

const goto_tracet & goto_trace_storaget::operator[] ( const irep_idt property_id) const

Definition at line 51 of file goto_trace_storage.cpp.

Member Data Documentation

◆ ns

const namespacet& goto_trace_storaget::ns
protected

the namespace related to the traces

Definition at line 38 of file goto_trace_storage.h.

◆ property_id_to_trace_index

std::unordered_map<irep_idt, std::size_t> goto_trace_storaget::property_id_to_trace_index
protected

Definition at line 44 of file goto_trace_storage.h.

◆ traces

std::vector<goto_tracet> goto_trace_storaget::traces
protected

stores the traces

Definition at line 41 of file goto_trace_storage.h.


The documentation for this class was generated from the following files: