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
16
#include <
util/decision_procedure.h
>
17
#include <
goto-programs/goto_trace.h
>
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
build_goto_trace
void build_goto_trace(const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Definition:
build_goto_trace.cpp:288
goto_trace.h
Traces of GOTO Programs.
decision_procedure.h
Decision Procedure Interface.
path_symex_state.h
State of path-based symbolic simulator.
decision_proceduret
Definition:
decision_procedure.h:20
goto_tracet
TO_BE_DOCUMENTED.
Definition:
goto_trace.h:146
path_symex_statet
Definition:
path_symex_state.h:21
path-symex
build_goto_trace.h
Generated by
1.8.14