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)
66 return std::string(numeric_cast_v<std::size_t>(*width),
'x');
78 out <<
"$date\n " << ctime(&t) <<
"$end" <<
"\n";
81 out <<
"$timescale 1 ns $end" <<
"\n";
87 for(
const auto &step : goto_trace.
steps)
89 if(step.is_assignment())
91 auto lhs_object=step.get_lhs_object();
92 if(lhs_object.has_value())
94 irep_idt identifier=lhs_object->get_identifier();
95 const typet &type=lhs_object->type();
97 const auto number=n.
number(identifier);
101 if(width.has_value() && (*width) >= 1)
102 out <<
"$var reg " << (*width) <<
" V" << number <<
" " << identifier
110 out <<
"$enddefinitions $end" <<
"\n";
112 unsigned timestamp=0;
114 for(
const auto &step : goto_trace.
steps)
120 auto lhs_object=step.get_lhs_object();
121 if(lhs_object.has_value())
123 irep_idt identifier=lhs_object->get_identifier();
124 const typet &type=lhs_object->type();
126 out <<
'#' << timestamp <<
"\n";
129 const auto number=n.
number(identifier);
132 if(type.
id()==ID_bool)
134 if(step.full_lhs_value.is_true())
135 out <<
"1" <<
"V" << number <<
"\n";
136 else if(step.full_lhs_value.is_false())
137 out <<
"0" <<
"V" << number <<
"\n";
139 out <<
"x" <<
"V" << number <<
"\n";
146 out <<
"b" <<
binary <<
" V" << number <<
" " <<
"\n";
The type of an expression, extends irept.
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
number_type number(const key_type &a)
typet & type()
Return the type of the expression.
Traces of GOTO Programs in VCD (Value Change Dump) Format.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define forall_operands(it, expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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 union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
static std::string binary(const constant_exprt &src)
const std::string & get_string(const irep_namet &name) const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)