cprover
Loading...
Searching...
No Matches
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.
void swap (goto_tracet &other)
void add_step (const goto_trace_stept &step)
 Add a step at the end of the trace.
goto_trace_steptget_last_step ()
 Retrieves the final step in the trace for manipulation (used to fill a trace from code, hence non-const)
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.

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 ( )
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 802 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 55 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: