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_stept >	stepst

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_stept &	get_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_stept &	get_last_step () const
std::set< irep_idt >	get_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

typedef std::list<goto_trace_stept> goto_tracet::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 805 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 58 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:

• /home/runner/work/cbmc/cbmc/src/goto-programs/goto_trace.h
• /home/runner/work/cbmc/cbmc/src/goto-programs/goto_trace.cpp