@@ -243,14 +243,15 @@ json_objectt json(
243
243
244
244
if (expr.id ()==ID_constant)
245
245
{
246
+ const constant_exprt &constant_expr=to_constant_expr (expr);
246
247
if (type.id ()==ID_unsignedbv ||
247
248
type.id ()==ID_signedbv ||
248
249
type.id ()==ID_c_bit_field)
249
250
{
250
251
std::size_t width=to_bitvector_type (type).get_width ();
251
252
252
253
result[" name" ]=json_stringt (" integer" );
253
- result[" binary" ]=json_stringt (expr. get_string (ID_value ));
254
+ result[" binary" ]=json_stringt (id2string (constant_expr. get_value () ));
254
255
result[" width" ]=json_numbert (std::to_string (width));
255
256
256
257
const typet &underlying_type=
@@ -279,7 +280,7 @@ json_objectt json(
279
280
else if (type.id ()==ID_c_enum)
280
281
{
281
282
result[" name" ]=json_stringt (" integer" );
282
- result[" binary" ]=json_stringt (expr. get_string (ID_value ));
283
+ result[" binary" ]=json_stringt (id2string (constant_expr. get_value () ));
283
284
result[" width" ]=json_numbert (type.subtype ().get_string (ID_width));
284
285
result[" c_type" ]=json_stringt (" enum" );
285
286
@@ -291,27 +292,27 @@ json_objectt json(
291
292
{
292
293
constant_exprt tmp;
293
294
tmp.type ()=ns.follow_tag (to_c_enum_tag_type (type));
294
- tmp.set_value (to_constant_expr (expr) .get_value ());
295
+ tmp.set_value (constant_expr .get_value ());
295
296
return json (tmp, ns);
296
297
}
297
298
else if (type.id ()==ID_bv)
298
299
{
299
300
result[" name" ]=json_stringt (" bitvector" );
300
- result[" binary" ]=json_stringt (expr. get_string (ID_value ));
301
+ result[" binary" ]=json_stringt (id2string (constant_expr. get_value () ));
301
302
}
302
303
else if (type.id ()==ID_fixedbv)
303
304
{
304
305
result[" name" ]=json_stringt (" fixed" );
305
306
result[" width" ]=json_numbert (type.get_string (ID_width));
306
- result[" binary" ]=json_stringt (expr. get_string (ID_value ));
307
+ result[" binary" ]=json_stringt (id2string (constant_expr. get_value () ));
307
308
result[" data" ]=
308
309
json_stringt (fixedbvt (to_constant_expr (expr)).to_ansi_c_string ());
309
310
}
310
311
else if (type.id ()==ID_floatbv)
311
312
{
312
313
result[" name" ]=json_stringt (" float" );
313
314
result[" width" ]=json_numbert (type.get_string (ID_width));
314
- result[" binary" ]=json_stringt (expr. get_string (ID_value ));
315
+ result[" binary" ]=json_stringt (id2string (constant_expr. get_value () ));
315
316
result[" data" ]=
316
317
json_stringt (ieee_floatt (to_constant_expr (expr)).to_ansi_c_string ());
317
318
}
@@ -350,7 +351,7 @@ json_objectt json(
350
351
else if (type.id ()==ID_string)
351
352
{
352
353
result[" name" ]=json_stringt (" string" );
353
- result[" data" ]=json_stringt (expr. get_string (ID_value ));
354
+ result[" data" ]=json_stringt (id2string (constant_expr. get_value () ));
354
355
}
355
356
else
356
357
{
0 commit comments