cprover
|
TO_BE_DOCUMENTED. More...
#include <goto_trace.h>
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 |
TO_BE_DOCUMENTED.
Definition at line 34 of file goto_trace.h.
typedef std::list<exprt> goto_trace_stept::io_argst |
Definition at line 113 of file goto_trace.h.
|
strong |
Enumerator | |
---|---|
STATE | |
ACTUAL_PARAMETER |
Definition at line 87 of file goto_trace.h.
|
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.
|
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().
|
inline |
Definition at line 41 of file goto_trace.h.
|
inline |
Definition at line 39 of file goto_trace.h.
References ASSIGNMENT, and type.
|
inline |
Definition at line 40 of file goto_trace.h.
|
inline |
Definition at line 55 of file goto_trace.h.
References ATOMIC_BEGIN, and type.
|
inline |
Definition at line 56 of file goto_trace.h.
References ATOMIC_END, and type.
|
inline |
Definition at line 43 of file goto_trace.h.
References CONSTRAINT, and type.
|
inline |
Definition at line 50 of file goto_trace.h.
|
inline |
Definition at line 49 of file goto_trace.h.
|
inline |
Definition at line 44 of file goto_trace.h.
References FUNCTION_CALL, and type.
|
inline |
Definition at line 45 of file goto_trace.h.
References FUNCTION_RETURN, and type.
|
inline |
Definition at line 42 of file goto_trace.h.
|
inline |
Definition at line 48 of file goto_trace.h.
|
inline |
Definition at line 46 of file goto_trace.h.
|
inline |
Definition at line 54 of file goto_trace.h.
References MEMORY_BARRIER, and type.
|
inline |
Definition at line 47 of file goto_trace.h.
|
inline |
Definition at line 51 of file goto_trace.h.
References SHARED_READ, and type.
|
inline |
Definition at line 52 of file goto_trace.h.
References SHARED_WRITE, and type.
|
inline |
Definition at line 53 of file goto_trace.h.
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.
assignment_typet goto_trace_stept::assignment_type |
Definition at line 88 of file goto_trace.h.
Referenced by build_goto_trace().
std::string goto_trace_stept::comment |
Definition at line 100 of file goto_trace.h.
Referenced by build_goto_trace(), and output().
exprt goto_trace_stept::cond_expr |
Definition at line 97 of file goto_trace.h.
Referenced by build_goto_trace(), and goto_trace_stept().
bool goto_trace_stept::cond_value |
Definition at line 96 of file goto_trace.h.
Referenced by build_goto_trace(), and output().
irep_idt goto_trace_stept::format_string |
Definition at line 112 of file goto_trace.h.
Referenced by build_goto_trace().
bool goto_trace_stept::formatted |
Definition at line 115 of file goto_trace.h.
Referenced by build_goto_trace().
exprt goto_trace_stept::full_lhs |
Definition at line 106 of file goto_trace.h.
Referenced by build_goto_trace(), and goto_trace_stept().
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().
bool goto_trace_stept::hidden |
Definition at line 84 of file goto_trace.h.
Referenced by build_goto_trace(), and output().
irep_idt goto_trace_stept::identifier |
Definition at line 118 of file goto_trace.h.
Referenced by build_goto_trace(), and output().
io_argst goto_trace_stept::io_args |
Definition at line 114 of file goto_trace.h.
Referenced by build_goto_trace().
irep_idt goto_trace_stept::io_id |
Definition at line 112 of file goto_trace.h.
Referenced by build_goto_trace().
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().
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().
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().
unsigned goto_trace_stept::step_nr |
Definition at line 37 of file goto_trace.h.
Referenced by build_goto_trace().
unsigned goto_trace_stept::thread_nr |
Definition at line 93 of file goto_trace.h.
Referenced by build_goto_trace(), and show_state_header().
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().