Adapt full_lhs_value to output binary for floating values

This is a precise representation of the floats, which can be useful

Author: Thomas Kiley

src/goto-programs/xml_goto_trace.cpp

@@ -19,10 +19,18 @@ Author: Daniel Kroening
 #include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
+#include <util/arith_tools.h>
 
 #include "printf_formatter.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"};
@@ -33,6 +41,13 @@ 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))
+  {
+    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);
+    full_lhs_value.set_attribute("binary", binary_representation);
+  }
   return full_lhs_value;
 }