CBMC
vcd_goto_trace.cpp File Reference

Traces of GOTO Programs in VCD (Value Change Dump) Format. More...

#include "vcd_goto_trace.h"
#include <ctime>
#include <util/arith_tools.h>
#include <util/numbering.h>
#include <util/pointer_offset_size.h>
#include "goto_trace.h"
+ Include dependency graph for vcd_goto_trace.cpp:

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)
 

Detailed Description

Traces of GOTO Programs in VCD (Value Change Dump) Format.

Definition in file vcd_goto_trace.cpp.

Function Documentation

◆ as_vcd_binary()

std::string as_vcd_binary ( const exprt expr,
const namespacet ns 
)

Definition at line 24 of file vcd_goto_trace.cpp.

◆ output_vcd()

void output_vcd ( const namespacet ns,
const goto_tracet goto_trace,
std::ostream &  out 
)

Definition at line 73 of file vcd_goto_trace.cpp.