CBMC
Loading...
Searching...
No Matches
vcd_goto_trace.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs in VCD (Value Change Dump) Format
4
5Author: Daniel Kroening
6
7Date: June 2011
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H
15#define CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H
16
17#include <iosfwd>
18
19class goto_tracet;
20class namespacet;
21
22void output_vcd(
23 const namespacet &ns,
24 const goto_tracet &goto_trace,
25 std::ostream &out);
26
27#endif // CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_tracet
Trace of a GOTO program.
Definition goto_trace.h:177
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
output_vcd
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Definition vcd_goto_trace.cpp:73