CBMC
Public Member Functions | Protected Attributes | List of all members
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_tracet & insert (goto_tracet &&)
 Store trace that ends in a violated assertion. More...
 
const goto_tracet & insert_all (goto_tracet &&)
 Store trace that contains multiple violated assertions. More...
 
const std::list< goto_tracet > & all () const
 
const goto_tracet & operator[] (const irep_idt &property_id) const
 
const namespacet & get_namespace () const
 

Protected Attributes

const namespacet & ns
 the namespace related to the traces More...
 
std::list< goto_tracet > traces
 stores the traces More...
 
std::unordered_map< irep_idt, std::size_t > property_id_to_trace_index
 
merge_irept merge_ireps
 irep container for shared ireps More...
 

Detailed Description

Definition at line 21 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::list< goto_tracet > & goto_trace_storaget::all ( ) const

Definition at line 54 of file goto_trace_storage.cpp.

◆ get_namespace()

const namespacet & goto_trace_storaget::get_namespace ( ) const

Definition at line 69 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 37 of file goto_trace_storage.cpp.

◆ operator[]()

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

Definition at line 59 of file goto_trace_storage.cpp.

Member Data Documentation

◆ merge_ireps

merge_irept goto_trace_storaget::merge_ireps
protected

irep container for shared ireps

Definition at line 51 of file goto_trace_storage.h.

◆ ns

const namespacet& goto_trace_storaget::ns
protected

the namespace related to the traces

Definition at line 42 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 48 of file goto_trace_storage.h.

◆ traces

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

stores the traces

Definition at line 45 of file goto_trace_storage.h.

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