TO_BE_DOCUMENTED.
More...
#include <goto_trace.h>
|
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 |
|
TO_BE_DOCUMENTED.
Definition at line 30 of file goto_trace.h.
◆ io_argst
◆ assignment_typet
Enumerator |
---|
STATE | |
ACTUAL_PARAMETER | |
Definition at line 86 of file goto_trace.h.
◆ typet
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.
◆ goto_trace_stept()
goto_trace_stept::goto_trace_stept |
( |
| ) |
|
|
inline |
◆ get_lhs_object()
◆ is_assert()
bool goto_trace_stept::is_assert |
( |
| ) |
const |
|
inline |
◆ is_assignment()
bool goto_trace_stept::is_assignment |
( |
| ) |
const |
|
inline |
◆ is_assume()
bool goto_trace_stept::is_assume |
( |
| ) |
const |
|
inline |
◆ is_atomic_begin()
bool goto_trace_stept::is_atomic_begin |
( |
| ) |
const |
|
inline |
◆ is_atomic_end()
bool goto_trace_stept::is_atomic_end |
( |
| ) |
const |
|
inline |
◆ is_constraint()
bool goto_trace_stept::is_constraint |
( |
| ) |
const |
|
inline |
◆ is_dead()
bool goto_trace_stept::is_dead |
( |
| ) |
const |
|
inline |
◆ is_decl()
bool goto_trace_stept::is_decl |
( |
| ) |
const |
|
inline |
◆ is_function_call()
bool goto_trace_stept::is_function_call |
( |
| ) |
const |
|
inline |
◆ is_function_return()
bool goto_trace_stept::is_function_return |
( |
| ) |
const |
|
inline |
◆ is_goto()
bool goto_trace_stept::is_goto |
( |
| ) |
const |
|
inline |
◆ is_input()
bool goto_trace_stept::is_input |
( |
| ) |
const |
|
inline |
◆ is_location()
bool goto_trace_stept::is_location |
( |
| ) |
const |
|
inline |
◆ is_memory_barrier()
bool goto_trace_stept::is_memory_barrier |
( |
| ) |
const |
|
inline |
◆ is_output()
bool goto_trace_stept::is_output |
( |
| ) |
const |
|
inline |
◆ is_shared_read()
bool goto_trace_stept::is_shared_read |
( |
| ) |
const |
|
inline |
◆ is_shared_write()
bool goto_trace_stept::is_shared_write |
( |
| ) |
const |
|
inline |
◆ is_spawn()
bool goto_trace_stept::is_spawn |
( |
| ) |
const |
|
inline |
◆ 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.
◆ assignment_type
◆ called_function
irep_idt goto_trace_stept::called_function |
◆ comment
std::string goto_trace_stept::comment |
◆ cond_expr
exprt goto_trace_stept::cond_expr |
◆ cond_value
bool goto_trace_stept::cond_value |
◆ format_string
irep_idt goto_trace_stept::format_string |
◆ formatted
bool goto_trace_stept::formatted |
◆ full_lhs
exprt goto_trace_stept::full_lhs |
◆ full_lhs_value
exprt goto_trace_stept::full_lhs_value |
◆ function
◆ function_arguments
std::vector<exprt> goto_trace_stept::function_arguments |
◆ hidden
bool goto_trace_stept::hidden |
◆ internal
bool goto_trace_stept::internal |
◆ io_args
◆ io_id
◆ pc
◆ step_nr
std::size_t goto_trace_stept::step_nr |
◆ thread_nr
unsigned goto_trace_stept::thread_nr |
◆ type
typet goto_trace_stept::type |
The documentation for this class was generated from the following files: