diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md
index 142ef548c4e..b5591cc4203 100644
--- a/doc/assets/xml_spec.md
+++ b/doc/assets/xml_spec.md
@@ -169,8 +169,10 @@ always present
- `full_lhs`: original lhs expression (after dereferencing)
- `full_lhs_value`: a constant with the new value.
- - if the type is a floating point number type, there will be an attribute`binary`
- showing its value.
+ - If the type of data can be represented as a fixed width sequence of bits
+ then, there will be an attribute `binary` containing the binary
+ representation. If the data type is signed and the value is negative
+ then the binary will be encoded using two's complement.
**Example**:
@@ -181,7 +183,7 @@ always present
signed int
b
- -1879048192
+ -1879048192
diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex
index 015b8e53dd3..9f9b7d56c91 100644
--- a/doc/assets/xml_spec.tex
+++ b/doc/assets/xml_spec.tex
@@ -149,8 +149,10 @@ \subsection{Trace Steps in XML}
\item \texttt{full\_lhs}: original lhs expression (after dereferencing)
\item \texttt{full\_lhs\_value}: a constant with the new value.
\begin{itemize}
- \item if the type is a floating point number type, there will be an attribute
- \texttt{binary} showing its value.
+ \item If the type of data can be represented as a fixed width sequence of bits
+ then, there will be an attribute \texttt{`binary`} containing the binary
+ representation. If the data type is signed and the value is negative
+ then the binary will be encoded using two's complement.
\end{itemize}
\end{itemize}
@@ -164,7 +166,7 @@ \subsection{Trace Steps in XML}
signed int
b
- -1879048192
+ -1879048192
diff --git a/regression/cbmc/integral-trace/test.c b/regression/cbmc/integral-trace/test.c
new file mode 100644
index 00000000000..508002d2e68
--- /dev/null
+++ b/regression/cbmc/integral-trace/test.c
@@ -0,0 +1,30 @@
+#include
+#include
+#include
+#include
+#include
+#include
+
+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;
+}
diff --git a/regression/cbmc/integral-trace/test.desc b/regression/cbmc/integral-trace/test.desc
new file mode 100644
index 00000000000..6584a02e66e
--- /dev/null
+++ b/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
+u8\s*97
+u16\s*8
+u32\s*16ul?
+u64\s*32ull?
+i1\s*2
+i2\s*3
+i3\s*4
+i4\s*5ll?
+in1\s*-2
+in2\s*-3
+in3\s*-4
+in4\s*-5ll?
+--
+--
+Checks that the binary value is printed for integral types.
diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
index 0fc03ee356c..cf2fe7e8135 100644
--- a/regression/cbmc/xml-trace/test.desc
+++ b/regression/cbmc/xml-trace/test.desc
@@ -8,7 +8,7 @@ VERIFICATION FAILED
union myunion
byte_extract_little_endian\(u, 0ll?, .*int.*\)
-\d+ll?
+\d+ll?
\{ \.i=\d+ll? \}
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
index bab0dfed78f..ae2a1439099 100644
--- a/src/goto-programs/xml_goto_trace.cpp
+++ b/src/goto-programs/xml_goto_trace.cpp
@@ -25,31 +25,34 @@ 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(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 exprt &value = step.full_lhs_value;
+ if(value.is_nil())
+ return value_xml;
const auto &lhs_object = step.get_lhs_object();
const irep_idt identifier =
lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
+ value_xml.data = from_expr(ns, identifier, value);
- 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 &bv_type = type_try_dynamic_cast(value.type());
+ const auto &constant = expr_try_dynamic_cast(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();
+ // It is fine to pass `false` into the `is_signed` parameter, even for
+ // signed values, because the subsequent conversion to binary will result
+ // in the same value either way. E.g. if the value is `-1` for a signed 8
+ // bit value, this will convert to `255` which is `11111111` in binary,
+ // which is the desired result.
+ 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(