Add binary representation to all bitvector values in the xml trace

Author: thomasspriggs

src/goto-programs/xml_goto_trace.cpp

@@ -25,13 +25,6 @@ Author: Daniel Kroening
 #include "structured_trace_util.h"
 #include "xml_expr.h"
 
-bool full_lhs_value_includes_binary(
-  const goto_trace_stept &step,
-  const namespacet &ns)
-{
-  return can_cast_type<floatbv_typet>(step.full_lhs_value.type());
-}
-
 xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
 {
   xmlt full_lhs_value{"full_lhs_value"};
@@ -42,11 +35,16 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
 
   if(step.full_lhs_value.is_not_nil())
     full_lhs_value.data = from_expr(ns, identifier, step.full_lhs_value);
-  if(full_lhs_value_includes_binary(step, ns))
+
+  if(
+    const auto &type =
+      type_try_dynamic_cast<bitvector_typet>(step.full_lhs_value.type()))
   {
-    const auto width = to_floatbv_type(step.full_lhs_value.type()).get_width();
-    const auto binary_representation = integer2binary(
-      bvrep2integer(step.full_lhs_value.get(ID_value), width, false), width);
+    const auto &constant =
+      expr_try_dynamic_cast<constant_exprt>(step.full_lhs_value);
+    const auto width = type->get_width();
+    const auto binary_representation =
+      integer2binary(bvrep2integer(constant->get_value(), width, false), width);
     full_lhs_value.set_attribute("binary", binary_representation);
   }
   return full_lhs_value;