cprover
build_goto_trace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Build Goto Trace from Path Symex History
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 // NOLINT(build/header_guard) as this file is also symlinked
13 #ifndef CPROVER_PATH_SYMEX_BUILD_GOTO_TRACE_H
14 #define CPROVER_PATH_SYMEX_BUILD_GOTO_TRACE_H
15 
18 
19 #include "path_symex_state.h"
20 
21 void build_goto_trace(
22  const path_symex_statet &state,
23  const decision_proceduret &decision_procedure,
24  goto_tracet &goto_trace);
25 
26 #endif // CPROVER_PATH_SYMEX_BUILD_GOTO_TRACE_H
void build_goto_trace(const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Traces of GOTO Programs.
Decision Procedure Interface.
State of path-based symbolic simulator.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146