cprover
|
Traces of GOTO Programs in VCD (Value Change Dump) Format. More...
#include "vcd_goto_trace.h"
#include <ctime>
#include <ostream>
#include <cassert>
#include <util/arith_tools.h>
#include <util/pointer_offset_size.h>
#include <util/numbering.h>
Go to the source code of this file.
Functions | |
std::string | as_vcd_binary (const exprt &expr, const namespacet &ns) |
void | output_vcd (const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out) |
Traces of GOTO Programs in VCD (Value Change Dump) Format.
Definition in file vcd_goto_trace.cpp.
std::string as_vcd_binary | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 24 of file vcd_goto_trace.cpp.
References namespace_baset::follow(), forall_operands, irept::get_string(), irept::id(), integer2size_t(), exprt::op0(), exprt::operands(), pointer_offset_size(), string2integer(), and exprt::type().
Referenced by output_vcd().
void output_vcd | ( | const namespacet & | ns, |
const goto_tracet & | goto_trace, | ||
std::ostream & | out | ||
) |
Definition at line 84 of file vcd_goto_trace.cpp.
References as_vcd_binary(), goto_trace_stept::ASSIGNMENT, irept::id(), numbering< T >::number(), pointer_offset_bits(), and goto_tracet::steps.