CBMC
goto_tracet Class Reference

Trace of a GOTO program. More...

#include <goto_trace.h>

+ Collaboration diagram for goto_tracet:

Public Types

typedef std::list< goto_trace_steptstepst
 

Public Member Functions

void clear ()
 
void output (const class namespacet &ns, std::ostream &out) const
 Outputs the trace in ASCII to a given stream. More...
 
void swap (goto_tracet &other)
 
void add_step (const goto_trace_stept &step)
 Add a step at the end of the trace. More...
 
goto_trace_steptget_last_step ()
 Retrieves the final step in the trace for manipulation (used to fill a trace from code, hence non-const) More...
 
const goto_trace_steptget_last_step () const
 
std::set< irep_idtget_failed_property_ids () const
 Returns the property IDs of all failed assertions in the trace. More...
 

Public Attributes

stepst steps
 

Detailed Description

Trace of a GOTO program.

This is a wrapper for a list of steps.

Definition at line 176 of file goto_trace.h.

Member Typedef Documentation

◆ stepst

Definition at line 179 of file goto_trace.h.

Member Function Documentation

◆ add_step()

void goto_tracet::add_step ( const goto_trace_stept step)
inline

Add a step at the end of the trace.

Definition at line 198 of file goto_trace.h.

◆ clear()

void goto_tracet::clear ( void  )
inline

Definition at line 182 of file goto_trace.h.

◆ get_failed_property_ids()

std::set< irep_idt > goto_tracet::get_failed_property_ids ( ) const

Returns the property IDs of all failed assertions in the trace.

Definition at line 804 of file goto_trace.cpp.

◆ get_last_step() [1/2]

goto_trace_stept& goto_tracet::get_last_step ( )
inline

Retrieves the final step in the trace for manipulation (used to fill a trace from code, hence non-const)

Definition at line 205 of file goto_trace.h.

◆ get_last_step() [2/2]

const goto_trace_stept& goto_tracet::get_last_step ( ) const
inline

Definition at line 210 of file goto_trace.h.

◆ output()

void goto_tracet::output ( const class namespacet ns,
std::ostream &  out 
) const

Outputs the trace in ASCII to a given stream.

Definition at line 57 of file goto_trace.cpp.

◆ swap()

void goto_tracet::swap ( goto_tracet other)
inline

Definition at line 192 of file goto_trace.h.

Member Data Documentation

◆ steps

stepst goto_tracet::steps

Definition at line 180 of file goto_trace.h.


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