Add binary representation to all bitvector values in the xml trace

regression/cbmc/integral-trace/test.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+#include <inttypes.h>
+#include <math.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdlib.h>
+
+int main()
+{
+  int8_t i1 = 2;
+  int16_t i2 = 3;
+  int32_t i3 = 4;
+  int64_t i4 = 5;
+
+  int8_t in1 = -2;
+  int16_t in2 = -3;
+  int32_t in3 = -4;
+  int64_t in4 = -5;
+
+  uint8_t u8 = 'a';
+  uint16_t u16 = 8;
+  uint32_t u32 = 16;
+  uint64_t u64 = 32;
+
+  void *ptr = malloc(1);
+
+  assert(false);
+
+  return 0;
+}

regression/cbmc/integral-trace/test.desc

@@ -0,0 +1,22 @@
+CORE
+test.c
+--trace --xml-ui
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs>u8</full_lhs>\s*<full_lhs_value binary="01100001">97</full_lhs_value>
+<full_lhs>u16</full_lhs>\s*<full_lhs_value binary="0{12}1000">8</full_lhs_value>
+<full_lhs>u32</full_lhs>\s*<full_lhs_value binary="0{27}10000">16ul?</full_lhs_value>
+<full_lhs>u64</full_lhs>\s*<full_lhs_value binary="0{58}100000">32ull?</full_lhs_value>
+<full_lhs>i1</full_lhs>\s*<full_lhs_value binary="0{6}10">2</full_lhs_value>
+<full_lhs>i2</full_lhs>\s*<full_lhs_value binary="0{14}11">3</full_lhs_value>
+<full_lhs>i3</full_lhs>\s*<full_lhs_value binary="0{29}100">4</full_lhs_value>
+<full_lhs>i4</full_lhs>\s*<full_lhs_value binary="0{61}101">5ll?</full_lhs_value>
+<full_lhs>in1</full_lhs>\s*<full_lhs_value binary="1{6}10">-2</full_lhs_value>
+<full_lhs>in2</full_lhs>\s*<full_lhs_value binary="1{14}01">-3</full_lhs_value>
+<full_lhs>in3</full_lhs>\s*<full_lhs_value binary="1{29}100">-4</full_lhs_value>
+<full_lhs>in4</full_lhs>\s*<full_lhs_value binary="1{61}011">-5ll?</full_lhs_value>
+--
+--
+Checks that the binary value is printed for integral types.

regression/cbmc/xml-trace/test.desc

@@ -8,7 +8,7 @@ VERIFICATION FAILED
 <location file=".*" function="test" line="\d+" working-directory=".*"/>
 <type>union myunion</type>
 <full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
-<full_lhs_value>\d+ll?</full_lhs_value>
+<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>
 <value>\{ \.i=\d+ll? \}</value>
 <value_expression>
 <union>

src/goto-programs/xml_goto_trace.cpp

@@ -25,31 +25,30 @@ 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"};
+  xmlt value_xml{"full_lhs_value"};
 
   const auto &lhs_object = step.get_lhs_object();
   const irep_idt identifier =
     lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
 
-  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(step.full_lhs_value.is_nil())
+    return value_xml;
+  value_xml.data = from_expr(ns, identifier, step.full_lhs_value);
+
+  const auto &bv_type =
+    type_try_dynamic_cast<bitvector_typet>(step.full_lhs_value.type());
+  const auto &constant =
+    expr_try_dynamic_cast<constant_exprt>(step.full_lhs_value);
+  if(bv_type && constant)
   {
-    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);
+    const auto width = bv_type->get_width();
+    const auto binary_representation =
+      integer2binary(bvrep2integer(constant->get_value(), width, false), width);
+    value_xml.set_attribute("binary", binary_representation);
   }
-  return full_lhs_value;
+  return value_xml;
 }
 
 void convert(