cprover
Public Types | Public Member Functions | Public Attributes | List of all members
goto_trace_stept Class Reference

TO_BE_DOCUMENTED. More...

#include <goto_trace.h>

Collaboration diagram for goto_trace_stept:
[legend]

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

unsigned step_nr
 
typet type
 
bool hidden
 
assignment_typet assignment_type
 
goto_programt::const_targett pc
 
unsigned thread_nr
 
bool cond_value
 
exprt cond_expr
 
std::string comment
 
ssa_exprt lhs_object
 
exprt full_lhs
 
exprt lhs_object_value
 
exprt full_lhs_value
 
irep_idt format_string
 
irep_idt io_id
 
io_argst io_args
 
bool formatted
 
irep_idt identifier
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 34 of file goto_trace.h.

Member Typedef Documentation

◆ io_argst

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

Definition at line 113 of file goto_trace.h.

Member Enumeration Documentation

◆ assignment_typet

enum goto_trace_stept::assignment_typet
strong
Enumerator
STATE 
ACTUAL_PARAMETER 

Definition at line 87 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 58 of file goto_trace.h.

Constructor & Destructor Documentation

◆ goto_trace_stept()

goto_trace_stept::goto_trace_stept ( )
inline

Definition at line 126 of file goto_trace.h.

References cond_expr, full_lhs, full_lhs_value, lhs_object, lhs_object_value, and irept::make_nil().

Member Function Documentation

◆ is_assert()

bool goto_trace_stept::is_assert ( ) const
inline

Definition at line 41 of file goto_trace.h.

References ASSERT, and type.

◆ is_assignment()

bool goto_trace_stept::is_assignment ( ) const
inline

Definition at line 39 of file goto_trace.h.

References ASSIGNMENT, and type.

◆ is_assume()

bool goto_trace_stept::is_assume ( ) const
inline

Definition at line 40 of file goto_trace.h.

References ASSUME, and type.

◆ is_atomic_begin()

bool goto_trace_stept::is_atomic_begin ( ) const
inline

Definition at line 55 of file goto_trace.h.

References ATOMIC_BEGIN, and type.

◆ is_atomic_end()

bool goto_trace_stept::is_atomic_end ( ) const
inline

Definition at line 56 of file goto_trace.h.

References ATOMIC_END, and type.

◆ is_constraint()

bool goto_trace_stept::is_constraint ( ) const
inline

Definition at line 43 of file goto_trace.h.

References CONSTRAINT, and type.

◆ is_dead()

bool goto_trace_stept::is_dead ( ) const
inline

Definition at line 50 of file goto_trace.h.

References DEAD, and type.

◆ is_decl()

bool goto_trace_stept::is_decl ( ) const
inline

Definition at line 49 of file goto_trace.h.

References DECL, and type.

◆ is_function_call()

bool goto_trace_stept::is_function_call ( ) const
inline

Definition at line 44 of file goto_trace.h.

References FUNCTION_CALL, and type.

◆ is_function_return()

bool goto_trace_stept::is_function_return ( ) const
inline

Definition at line 45 of file goto_trace.h.

References FUNCTION_RETURN, and type.

◆ is_goto()

bool goto_trace_stept::is_goto ( ) const
inline

Definition at line 42 of file goto_trace.h.

References GOTO, and type.

◆ is_input()

bool goto_trace_stept::is_input ( ) const
inline

Definition at line 48 of file goto_trace.h.

References INPUT, and type.

◆ is_location()

bool goto_trace_stept::is_location ( ) const
inline

Definition at line 46 of file goto_trace.h.

References LOCATION, and type.

◆ is_memory_barrier()

bool goto_trace_stept::is_memory_barrier ( ) const
inline

Definition at line 54 of file goto_trace.h.

References MEMORY_BARRIER, and type.

◆ is_output()

bool goto_trace_stept::is_output ( ) const
inline

Definition at line 47 of file goto_trace.h.

References OUTPUT, and type.

◆ is_shared_read()

bool goto_trace_stept::is_shared_read ( ) const
inline

Definition at line 51 of file goto_trace.h.

References SHARED_READ, and type.

◆ is_shared_write()

bool goto_trace_stept::is_shared_write ( ) const
inline

Definition at line 52 of file goto_trace.h.

References SHARED_WRITE, and type.

◆ is_spawn()

bool goto_trace_stept::is_spawn ( ) const
inline

Definition at line 53 of file goto_trace.h.

References SPAWN, and type.

◆ 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 33 of file goto_trace.cpp.

References ASSERT, ASSIGNMENT, ASSUME, ATOMIC_BEGIN, ATOMIC_END, comment, cond_value, DECL, from_expr(), FUNCTION_CALL, FUNCTION_RETURN, ssa_exprt::get_object_name(), ssa_exprt::get_original_expr(), GOTO, hidden, identifier, INPUT, lhs_object, lhs_object_value, LOCATION, OUTPUT, pc, SHARED_READ, SHARED_WRITE, and type.

Member Data Documentation

◆ assignment_type

assignment_typet goto_trace_stept::assignment_type

Definition at line 88 of file goto_trace.h.

Referenced by build_goto_trace().

◆ comment

std::string goto_trace_stept::comment

Definition at line 100 of file goto_trace.h.

Referenced by build_goto_trace(), and output().

◆ cond_expr

exprt goto_trace_stept::cond_expr

Definition at line 97 of file goto_trace.h.

Referenced by build_goto_trace(), and goto_trace_stept().

◆ cond_value

bool goto_trace_stept::cond_value

Definition at line 96 of file goto_trace.h.

Referenced by build_goto_trace(), and output().

◆ format_string

irep_idt goto_trace_stept::format_string

Definition at line 112 of file goto_trace.h.

Referenced by build_goto_trace().

◆ formatted

bool goto_trace_stept::formatted

Definition at line 115 of file goto_trace.h.

Referenced by build_goto_trace().

◆ full_lhs

exprt goto_trace_stept::full_lhs

Definition at line 106 of file goto_trace.h.

Referenced by build_goto_trace(), and goto_trace_stept().

◆ full_lhs_value

exprt goto_trace_stept::full_lhs_value

Definition at line 109 of file goto_trace.h.

Referenced by build_goto_trace(), and goto_trace_stept().

◆ hidden

bool goto_trace_stept::hidden

Definition at line 84 of file goto_trace.h.

Referenced by build_goto_trace(), and output().

◆ identifier

irep_idt goto_trace_stept::identifier

Definition at line 118 of file goto_trace.h.

Referenced by build_goto_trace(), and output().

◆ io_args

io_argst goto_trace_stept::io_args

Definition at line 114 of file goto_trace.h.

Referenced by build_goto_trace().

◆ io_id

irep_idt goto_trace_stept::io_id

Definition at line 112 of file goto_trace.h.

Referenced by build_goto_trace().

◆ lhs_object

ssa_exprt goto_trace_stept::lhs_object

Definition at line 103 of file goto_trace.h.

Referenced by build_goto_trace(), goto_trace_stept(), and output().

◆ lhs_object_value

exprt goto_trace_stept::lhs_object_value

Definition at line 109 of file goto_trace.h.

Referenced by build_goto_trace(), goto_trace_stept(), and output().

◆ pc

goto_programt::const_targett goto_trace_stept::pc

Definition at line 90 of file goto_trace.h.

Referenced by build_goto_trace(), bmct::error_trace(), and output().

◆ step_nr

unsigned goto_trace_stept::step_nr

Definition at line 37 of file goto_trace.h.

Referenced by build_goto_trace().

◆ thread_nr

unsigned goto_trace_stept::thread_nr

Definition at line 93 of file goto_trace.h.

Referenced by build_goto_trace(), and show_state_header().

◆ type

typet goto_trace_stept::type

Definition at line 81 of file goto_trace.h.

Referenced by build_goto_trace(), 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(), and output().

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