Go to the documentation of this file.
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)
116 if(step.is_assignment())
118 auto lhs_object = step.get_lhs_object();
119 if(lhs_object.has_value())
121 irep_idt identifier = lhs_object->get_identifier();
122 const typet &type = lhs_object->type();
124 out <<
'#' << timestamp <<
"\n";
127 const auto number = n.
number(identifier);
130 if(type.
id() == ID_bool)
132 if(step.full_lhs_value.is_true())
134 <<
"V" << number <<
"\n";
135 else if(step.full_lhs_value.is_false())
137 <<
"V" << number <<
"\n";
140 <<
"V" << number <<
"\n";
147 out <<
"b" <<
binary <<
" V" << number <<
" "
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The type of an expression, extends irept.
Base class for all expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
std::string as_vcd_binary(const exprt &expr, const namespacet &ns)
Traces of GOTO Programs in VCD (Value Change Dump) Format.
number_type number(const key_type &a)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
#define forall_operands(it, expr)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const irep_idt & id() const
const std::string & get_string(const irep_namet &name) const
void output_vcd(const namespacet &ns, const goto_tracet &goto_trace, std::ostream &out)
static std::string binary(const constant_exprt &src)