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 | |
std::size_t | step_nr |
typet | type |
bool | hidden |
bool | internal |
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 36 of file goto_trace.h.
typedef std::list<exprt> goto_trace_stept::io_argst |
Definition at line 118 of file goto_trace.h.
|
strong |
Enumerator | |
---|---|
STATE | |
ACTUAL_PARAMETER |
Definition at line 92 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 60 of file goto_trace.h.
|
inline |
Definition at line 131 of file goto_trace.h.
References cond_expr, full_lhs, full_lhs_value, lhs_object, lhs_object_value, and irept::make_nil().
|
inline |
|
inline |
Definition at line 41 of file goto_trace.h.
References ASSIGNMENT, and type.
Referenced by output().
|
inline |
|
inline |
Definition at line 57 of file goto_trace.h.
References ATOMIC_BEGIN, and type.
|
inline |
Definition at line 58 of file goto_trace.h.
References ATOMIC_END, and type.
|
inline |
Definition at line 45 of file goto_trace.h.
References CONSTRAINT, and type.
|
inline |
Definition at line 52 of file goto_trace.h.
|
inline |
Definition at line 51 of file goto_trace.h.
|
inline |
Definition at line 46 of file goto_trace.h.
References FUNCTION_CALL, and type.
Referenced by output().
|
inline |
Definition at line 47 of file goto_trace.h.
References FUNCTION_RETURN, and type.
Referenced by output().
|
inline |
|
inline |
Definition at line 50 of file goto_trace.h.
|
inline |
Definition at line 48 of file goto_trace.h.
|
inline |
Definition at line 56 of file goto_trace.h.
References MEMORY_BARRIER, and type.
|
inline |
Definition at line 49 of file goto_trace.h.
|
inline |
Definition at line 53 of file goto_trace.h.
References SHARED_READ, and type.
|
inline |
Definition at line 54 of file goto_trace.h.
References SHARED_WRITE, and type.
|
inline |
Definition at line 55 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 35 of file goto_trace.cpp.
References ASSERT, ASSIGNMENT, ASSUME, ATOMIC_BEGIN, ATOMIC_END, comment, cond_value, DEAD, DECL, format(), full_lhs, full_lhs_value, FUNCTION_CALL, FUNCTION_RETURN, GOTO, hidden, identifier, INPUT, is_assert(), is_assignment(), is_assume(), is_function_call(), is_function_return(), is_goto(), LOCATION, OUTPUT, pc, SHARED_READ, SHARED_WRITE, type, and UNREACHABLE.
assignment_typet goto_trace_stept::assignment_type |
Definition at line 93 of file goto_trace.h.
Referenced by build_goto_trace(), and convert_decl().
std::string goto_trace_stept::comment |
Definition at line 105 of file goto_trace.h.
Referenced by build_goto_trace(), convert_assert(), and output().
exprt goto_trace_stept::cond_expr |
Definition at line 102 of file goto_trace.h.
Referenced by build_goto_trace(), and goto_trace_stept().
bool goto_trace_stept::cond_value |
Definition at line 101 of file goto_trace.h.
Referenced by build_goto_trace(), and output().
irep_idt goto_trace_stept::format_string |
Definition at line 117 of file goto_trace.h.
Referenced by build_goto_trace().
bool goto_trace_stept::formatted |
Definition at line 120 of file goto_trace.h.
Referenced by build_goto_trace().
exprt goto_trace_stept::full_lhs |
Definition at line 111 of file goto_trace.h.
Referenced by build_goto_trace(), convert_decl(), interpretert::execute_assign(), goto_trace_stept(), and output().
exprt goto_trace_stept::full_lhs_value |
Definition at line 114 of file goto_trace.h.
Referenced by build_goto_trace(), convert_decl(), interpretert::execute_assign(), goto_trace_stept(), and output().
bool goto_trace_stept::hidden |
Definition at line 86 of file goto_trace.h.
Referenced by build_goto_trace(), convert_assert(), convert_decl(), convert_default(), convert_input(), convert_output(), convert_return(), and output().
irep_idt goto_trace_stept::identifier |
Definition at line 123 of file goto_trace.h.
Referenced by build_goto_trace(), convert_return(), interpretert::execute_function_call(), and output().
bool goto_trace_stept::internal |
Definition at line 89 of file goto_trace.h.
Referenced by convert_assert(), convert_decl(), convert_input(), convert_output(), convert_return(), set_internal_dynamic_object(), and update_internal_field().
io_argst goto_trace_stept::io_args |
Definition at line 119 of file goto_trace.h.
Referenced by build_goto_trace(), convert_input(), and convert_output().
irep_idt goto_trace_stept::io_id |
Definition at line 117 of file goto_trace.h.
Referenced by build_goto_trace(), convert_input(), and convert_output().
ssa_exprt goto_trace_stept::lhs_object |
Definition at line 108 of file goto_trace.h.
Referenced by build_goto_trace(), convert_decl(), interpretert::execute_assign(), and goto_trace_stept().
exprt goto_trace_stept::lhs_object_value |
Definition at line 114 of file goto_trace.h.
Referenced by build_goto_trace(), interpretert::execute_assign(), and goto_trace_stept().
goto_programt::const_targett goto_trace_stept::pc |
Definition at line 95 of file goto_trace.h.
Referenced by build_goto_trace(), convert_assert(), convert_input(), convert_output(), bmct::error_trace(), output(), and interpretert::step().
std::size_t goto_trace_stept::step_nr |
Definition at line 39 of file goto_trace.h.
unsigned goto_trace_stept::thread_nr |
Definition at line 98 of file goto_trace.h.
Referenced by build_goto_trace(), convert_assert(), convert_decl(), convert_default(), convert_input(), convert_output(), convert_return(), show_state_header(), and interpretert::step().
typet goto_trace_stept::type |
Definition at line 83 of file goto_trace.h.
Referenced by build_goto_trace(), convert_return(), 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(), interpretert::step(), and update_internal_field().