|
23 | 23 | #include <langapi/language_util.h>
|
24 | 24 | #include <util/range.h>
|
25 | 25 | #include <goto-symex/renamed.h>
|
| 26 | +#include <util/format_expr.h> |
| 27 | +#include <util/format_type.h> |
26 | 28 |
|
27 | 29 | #ifdef DEBUG
|
28 | 30 | #include <iostream>
|
@@ -134,7 +136,7 @@ bool value_sett::insert(
|
134 | 136 | }
|
135 | 137 |
|
136 | 138 | void value_sett::output(
|
137 |
| - const namespacet &ns, |
| 139 | + const namespacet &, |
138 | 140 | std::ostream &out,
|
139 | 141 | const std::string &indent) const
|
140 | 142 | {
|
@@ -175,29 +177,29 @@ void value_sett::output(
|
175 | 177 | {
|
176 | 178 | const exprt &o = object_numbering[o_it->first];
|
177 | 179 |
|
178 |
| - std::string result; |
| 180 | + std::ostringstream stream; |
179 | 181 |
|
180 | 182 | if(o.id() == ID_invalid || o.id() == ID_unknown)
|
181 |
| - result = from_expr(ns, identifier, o); |
| 183 | + stream << format(o); |
182 | 184 | else
|
183 | 185 | {
|
184 |
| - result = "<" + from_expr(ns, identifier, o) + ", "; |
| 186 | + stream << "<" << format(o) << ", "; |
185 | 187 |
|
186 | 188 | if(o_it->second)
|
187 |
| - result += integer2string(*o_it->second); |
| 189 | + stream << *o_it->second; |
188 | 190 | else
|
189 |
| - result += '*'; |
| 191 | + stream << '*'; |
190 | 192 |
|
191 | 193 | if(o.type().is_nil())
|
192 |
| - result += ", ?"; |
| 194 | + stream << ", ?"; |
193 | 195 | else
|
194 |
| - result += ", " + from_type(ns, identifier, o.type()); |
| 196 | + stream << ", " << format(o.type()); |
195 | 197 |
|
196 |
| - result += '>'; |
| 198 | + stream << '>'; |
197 | 199 | }
|
198 | 200 |
|
| 201 | + const std::string result = stream.str(); |
199 | 202 | out << result;
|
200 |
| - |
201 | 203 | width += result.size();
|
202 | 204 |
|
203 | 205 | object_map_dt::const_iterator next(o_it);
|
|
0 commit comments