cprover
build_goto_trace.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Traces of GOTO Programs
4
5
Author: Daniel Kroening
6
7
Date: July 2005
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
15
#define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
16
17
#include "
symex_target_equation.h
"
18
#include "
goto_symex_state.h
"
19
20
// builds a trace that stops at first failing assertion
21
void
build_goto_trace
(
22
const
symex_target_equationt
&target,
23
const
prop_convt
&prop_conv,
24
const
namespacet
&ns,
25
goto_tracet
&goto_trace);
26
27
// builds a trace that stops after given step
28
void
build_goto_trace
(
29
const
symex_target_equationt
&target,
30
symex_target_equationt::SSA_stepst::const_iterator stop,
31
const
prop_convt
&prop_conv,
32
const
namespacet
&ns,
33
goto_tracet
&goto_trace);
34
35
#endif // CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
symex_target_equation.h
Generate Equation using Symbolic Execution.
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
symex_target_equationt
Definition:
symex_target_equation.h:31
goto_symex_state.h
Symbolic Execution.
prop_convt
Definition:
prop_conv.h:27
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
goto_tracet
TO_BE_DOCUMENTED.
Definition:
goto_trace.h:146
goto-symex
build_goto_trace.h
Generated by
1.8.14