28 if(expr.
id()==ID_constant)
30 if(type.
id()==ID_unsignedbv ||
31 type.
id()==ID_signedbv ||
33 type.
id()==ID_fixedbv ||
34 type.
id()==ID_floatbv ||
35 type.
id()==ID_pointer)
38 else if(expr.
id()==ID_array)
47 else if(expr.
id()==ID_struct)
56 else if(expr.
id()==ID_union)
79 out <<
"$date\n " << ctime(&t) <<
"$end" <<
"\n";
82 out <<
"$timescale 1 ns $end" <<
"\n";
88 for(
const auto &step : goto_trace.
steps)
90 if(step.is_assignment())
92 irep_idt identifier=step.lhs_object.get_identifier();
93 const typet &type=step.lhs_object.type();
95 const auto number=n.
number(identifier);
100 out <<
"$var reg " << width <<
" V" << number <<
" " 101 << identifier <<
" $end" <<
"\n";
106 out <<
"$enddefinitions $end" <<
"\n";
108 unsigned timestamp=0;
110 for(
const auto &step : goto_trace.
steps)
116 irep_idt identifier=step.lhs_object.get_identifier();
117 const typet &type=step.lhs_object.type();
119 out <<
'#' << timestamp <<
"\n";
122 const auto number=n.
number(identifier);
125 if(type.
id()==ID_bool)
127 if(step.lhs_object_value.is_true())
128 out <<
"1" <<
"V" << number <<
"\n";
129 else if(step.lhs_object_value.is_false())
130 out <<
"0" <<
"V" << number <<
"\n";
132 out <<
"x" <<
"V" << number <<
"\n";
139 out <<
"b" << binary <<
" V" << number <<
" " <<
"\n";
The type of an expression.
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
number_type number(const key_type &a)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
Traces of GOTO Programs in VCD (Value Change Dump) Format.
const irep_idt & id() const
#define forall_operands(it, expr)
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
Base class for all expressions.
const std::string & get_string(const irep_namet &name) const
std::size_t integer2size_t(const mp_integer &n)