TO_BE_DOCUMENTED. More...

#include <goto_trace.h>

Collaboration diagram for goto_trace_stept:

Public Types
enum	typet { typet::NONE, typet::ASSIGNMENT, typet::ASSUME, typet::ASSERT, typet::GOTO, typet::LOCATION, typet::INPUT, typet::OUTPUT, typet::DECL, typet::DEAD, typet::FUNCTION_CALL, typet::FUNCTION_RETURN, typet::CONSTRAINT, typet::SHARED_READ, typet::SHARED_WRITE, typet::SPAWN, typet::MEMORY_BARRIER, typet::ATOMIC_BEGIN, typet::ATOMIC_END }

enum	assignment_typet { assignment_typet::STATE, assignment_typet::ACTUAL_PARAMETER }

typedef std::list< exprt >	io_argst

Public Member Functions
bool	is_assignment () const

bool	is_assume () const

bool	is_assert () const

bool	is_goto () const

bool	is_constraint () const

bool	is_function_call () const

bool	is_function_return () const

bool	is_location () const

bool	is_output () const

bool	is_input () const

bool	is_decl () const

bool	is_dead () const

bool	is_shared_read () const

bool	is_shared_write () const

bool	is_spawn () const

bool	is_memory_barrier () const

bool	is_atomic_begin () const

bool	is_atomic_end () const

optionalt< symbol_exprt >	get_lhs_object () const

void	output (const class namespacet &ns, std::ostream &out) const
	outputs the trace step in ASCII to a given stream More...

	goto_trace_stept ()

Public Attributes
std::size_t	step_nr

typet	type

bool	hidden

bool	internal

assignment_typet	assignment_type

irep_idt	function

goto_programt::const_targett	pc

unsigned	thread_nr

bool	cond_value

exprt	cond_expr

std::string	comment

exprt	full_lhs

exprt	full_lhs_value

irep_idt	format_string

irep_idt	io_id

io_argst	io_args

bool	formatted

irep_idt	called_function

std::vector< exprt >	function_arguments

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 30 of file goto_trace.h.

Member Typedef Documentation

◆ io_argst

typedef std::list<exprt> goto_trace_stept::io_argst

Definition at line 115 of file goto_trace.h.

Member Enumeration Documentation

◆ assignment_typet

enum goto_trace_stept::assignment_typet

strong

Enumerator
STATE
ACTUAL_PARAMETER

Definition at line 86 of file goto_trace.h.

◆ typet

enum goto_trace_stept::typet

strong

Enumerator
NONE
ASSIGNMENT
ASSUME
ASSERT
GOTO
LOCATION
INPUT
OUTPUT
DECL
DEAD
FUNCTION_CALL
FUNCTION_RETURN
CONSTRAINT
SHARED_READ
SHARED_WRITE
SPAWN
MEMORY_BARRIER
ATOMIC_BEGIN
ATOMIC_END

Definition at line 54 of file goto_trace.h.

Constructor & Destructor Documentation

◆ goto_trace_stept()

goto_trace_stept::goto_trace_stept ( )

inline

Definition at line 131 of file goto_trace.h.

Member Function Documentation

◆ get_lhs_object()

optionalt< symbol_exprt > goto_trace_stept::get_lhs_object ( ) const

Definition at line 42 of file goto_trace.cpp.

◆ is_assert()

bool goto_trace_stept::is_assert ( ) const

inline

Definition at line 37 of file goto_trace.h.

◆ is_assignment()

bool goto_trace_stept::is_assignment ( ) const

inline

Definition at line 35 of file goto_trace.h.

◆ is_assume()

bool goto_trace_stept::is_assume ( ) const

inline

Definition at line 36 of file goto_trace.h.

◆ is_atomic_begin()

bool goto_trace_stept::is_atomic_begin ( ) const

inline

Definition at line 51 of file goto_trace.h.

◆ is_atomic_end()

bool goto_trace_stept::is_atomic_end ( ) const

inline

Definition at line 52 of file goto_trace.h.

◆ is_constraint()

bool goto_trace_stept::is_constraint ( ) const

inline

Definition at line 39 of file goto_trace.h.

◆ is_dead()

bool goto_trace_stept::is_dead ( ) const

inline

Definition at line 46 of file goto_trace.h.

◆ is_decl()

bool goto_trace_stept::is_decl ( ) const

inline

Definition at line 45 of file goto_trace.h.

◆ is_function_call()

bool goto_trace_stept::is_function_call ( ) const

inline

Definition at line 40 of file goto_trace.h.

◆ is_function_return()

bool goto_trace_stept::is_function_return ( ) const

inline

Definition at line 41 of file goto_trace.h.

◆ is_goto()

bool goto_trace_stept::is_goto ( ) const

inline

Definition at line 38 of file goto_trace.h.

◆ is_input()

bool goto_trace_stept::is_input ( ) const

inline

Definition at line 44 of file goto_trace.h.

◆ is_location()

bool goto_trace_stept::is_location ( ) const

inline

Definition at line 42 of file goto_trace.h.

◆ is_memory_barrier()

bool goto_trace_stept::is_memory_barrier ( ) const

inline

Definition at line 50 of file goto_trace.h.

◆ is_output()

bool goto_trace_stept::is_output ( ) const

inline

Definition at line 43 of file goto_trace.h.

◆ is_shared_read()

bool goto_trace_stept::is_shared_read ( ) const

inline

Definition at line 47 of file goto_trace.h.

◆ is_shared_write()

bool goto_trace_stept::is_shared_write ( ) const

inline

Definition at line 48 of file goto_trace.h.

◆ is_spawn()

bool goto_trace_stept::is_spawn ( ) const

inline

Definition at line 49 of file goto_trace.h.

◆ output()

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

outputs the trace step in ASCII to a given stream

Definition at line 55 of file goto_trace.cpp.

Member Data Documentation

◆ assignment_type

assignment_typet goto_trace_stept::assignment_type

Definition at line 87 of file goto_trace.h.

◆ called_function

irep_idt goto_trace_stept::called_function

Definition at line 120 of file goto_trace.h.

◆ comment

std::string goto_trace_stept::comment

Definition at line 102 of file goto_trace.h.

◆ cond_expr

exprt goto_trace_stept::cond_expr

Definition at line 99 of file goto_trace.h.

◆ cond_value

bool goto_trace_stept::cond_value

Definition at line 98 of file goto_trace.h.

◆ format_string

irep_idt goto_trace_stept::format_string

Definition at line 114 of file goto_trace.h.

◆ formatted

bool goto_trace_stept::formatted

Definition at line 117 of file goto_trace.h.

◆ full_lhs

exprt goto_trace_stept::full_lhs

Definition at line 105 of file goto_trace.h.

◆ full_lhs_value

exprt goto_trace_stept::full_lhs_value

Definition at line 111 of file goto_trace.h.

◆ function

irep_idt goto_trace_stept::function

Definition at line 91 of file goto_trace.h.

◆ function_arguments

std::vector<exprt> goto_trace_stept::function_arguments

Definition at line 123 of file goto_trace.h.

◆ hidden

bool goto_trace_stept::hidden

Definition at line 80 of file goto_trace.h.

◆ internal

bool goto_trace_stept::internal

Definition at line 83 of file goto_trace.h.

◆ io_args

io_argst goto_trace_stept::io_args

Definition at line 116 of file goto_trace.h.

◆ io_id

irep_idt goto_trace_stept::io_id

Definition at line 114 of file goto_trace.h.

◆ pc

goto_programt::const_targett goto_trace_stept::pc

Definition at line 92 of file goto_trace.h.

◆ step_nr

std::size_t goto_trace_stept::step_nr

Definition at line 33 of file goto_trace.h.

◆ thread_nr

unsigned goto_trace_stept::thread_nr

Definition at line 95 of file goto_trace.h.

◆ type

typet goto_trace_stept::type

Definition at line 77 of file goto_trace.h.

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

goto-programs/goto_trace.h
goto-programs/goto_trace.cpp

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ io_argst

Member Enumeration Documentation

◆ assignment_typet

◆ typet

Constructor & Destructor Documentation

◆ goto_trace_stept()

Member Function Documentation

◆ get_lhs_object()

◆ is_assert()

◆ is_assignment()

◆ is_assume()

◆ is_atomic_begin()

◆ is_atomic_end()

◆ is_constraint()

◆ is_dead()

◆ is_decl()

◆ is_function_call()

◆ is_function_return()

◆ is_goto()

◆ is_input()

◆ is_location()

◆ is_memory_barrier()

◆ is_output()

◆ is_shared_read()

◆ is_shared_write()

◆ is_spawn()

◆ output()

Member Data Documentation

◆ assignment_type

◆ called_function

◆ comment

◆ cond_expr

◆ cond_value

◆ format_string

◆ formatted

◆ full_lhs

◆ full_lhs_value

◆ function

◆ function_arguments

◆ hidden

◆ internal

◆ io_args

◆ io_id

◆ pc

◆ step_nr

◆ thread_nr

◆ type