cprover
|
Build Goto Trace from Path Symex History. More...
#include <util/decision_procedure.h>
#include <goto-programs/goto_trace.h>
#include "path_symex_state.h"
Go to the source code of this file.
Functions | |
void | build_goto_trace (const path_symex_statet &state, const decision_proceduret &decision_procedure, goto_tracet &goto_trace) |
follow state history to build a goto trace More... | |
Build Goto Trace from Path Symex History.
Definition in file build_goto_trace.h.
void build_goto_trace | ( | const path_symex_statet & | state, |
const decision_proceduret & | decision_procedure, | ||
goto_tracet & | goto_trace | ||
) |
follow state history to build a goto trace
Definition at line 15 of file build_goto_trace.cpp.
References goto_tracet::add_step(), goto_trace_stept::ASSERT, ASSIGN, goto_trace_stept::ASSIGNMENT, ASSUME, goto_trace_stept::ASSUME, ATOMIC_BEGIN, goto_trace_stept::ATOMIC_BEGIN, ATOMIC_END, goto_trace_stept::ATOMIC_END, path_symex_step_reft::build_history(), goto_trace_stept::comment, comment(), DEAD, goto_trace_stept::DEAD, DECL, goto_trace_stept::DECL, dstringt::empty(), END_FUNCTION, goto_trace_stept::full_lhs, path_symex_stept::full_lhs, goto_trace_stept::full_lhs_value, FUNCTION_CALL, goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, decision_proceduret::get(), path_symex_statet::get_current_thread(), path_symex_statet::get_instruction(), path_symex_statet::history, id2string(), loc_reft::is_nil(), goto_trace_stept::lhs_object, goto_trace_stept::LOCATION, path_symex_statet::locs, goto_trace_stept::pc, path_symex_stept::pc, goto_trace_stept::SPAWN, path_symex_stept::ssa_lhs, START_THREAD, goto_trace_stept::step_nr, goto_trace_stept::thread_nr, path_symex_stept::thread_nr, and goto_trace_stept::type.