Adapt the XSD to include the binary output

Also updat the LaTeX and markdown documentation to include the new
attribute

Author: Thomas Kiley

doc/assets/xml_spec.md

@@ -168,7 +168,9 @@ always present
 
 -   `full_lhs`: original lhs expression (after dereferencing)
 
--   `full_lhs_value`: a constant with the new value
+-   `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.
 
 **Example**:
 
@@ -181,6 +183,12 @@ always present
   <full_lhs>b</full_lhs>
   <full_lhs_value>-1879048192</full_lhs_value>
 </assignment>
+<assignment assignment_type="state" base_name="d" display_name="main::1::d" hidden="false" identifier="main::1::d" mode="C" step_nr="26" thread="0">
+  <location file="main.i" function="main" line="3" working-directory="/home/tkiley/workspace/cbmc/regression/cbmc/Float24"/>
+  <type>double</type>
+  <full_lhs>d</full_lhs>
+  <full_lhs_value binary="0100000000010100011001100110011001100110011001100110011001100110">5.1</full_lhs_value>
+</assignment>
 ```
 
 **XSD**:
@@ -192,7 +200,15 @@ always present
       <xs:element name="location" minOccurs="0"></xs:element>
       <xs:element name="type" type="xs:string" minOccurs="0"></xs:element>
       <xs:element name="full_lhs" type="xs:string"></xs:element>
-      <xs:element name="full_lhs_value" type="xs:int"></xs:element>
+      <xs:element name="full_lhs_value">
+        <xs:complexType>
+          <xs:simpleContent>
+            <xs:extension base="xs:string">
+              <xs:attribute name="binary" type="xs:string"/>
+            </xs:extension>
+          </xs:simpleContent>
+        </xs:complexType>
+      </xs:element>
     </xs:all>
     <xs:attributeGroup ref="traceStepAttrs">
     <xs:attribute name="assignment_type" type="xs:string"></xs:attribute>

doc/assets/xml_spec.tex

@@ -147,9 +147,15 @@ \subsection{Trace Steps in XML}
 always present
 \begin{itemize}
 \item \texttt{full\_lhs}: original lhs expression (after dereferencing)
-\item \texttt{full\_lhs\_value}: a constant with the new value
+\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.
+  \end{itemize}
+
 \end{itemize}
 
+
 \noindent\textbf{Example}:
 \begin{minted}{xml}
 <assignment assignment_type="state" base_name="b" display_name="main::1::b"
@@ -160,6 +166,13 @@ \subsection{Trace Steps in XML}
   <full_lhs>b</full_lhs>
   <full_lhs_value>-1879048192</full_lhs_value>
 </assignment>
+<assignment assignment_type="state" base_name="d" display_name="main::1::d" hidden="false" identifier="main::1::d" mode="C" step_nr="26" thread="0">
+  <location ../>
+  <type>double</type>
+  <full_lhs>d</full_lhs>
+  <full_lhs_value
+binary="0100000000010100011001100110011001100110011001100110011001100110">5.1</full_lhs_value>
+</assignment>
 \end{minted}
 
 \noindent\textbf{XSD}:
@@ -170,7 +183,15 @@ \subsection{Trace Steps in XML}
       <xs:element name="location" minOccurs="0"></xs:element>
       <xs:element name="type" type="xs:string" minOccurs="0"></xs:element>
       <xs:element name="full_lhs" type="xs:string"></xs:element>
-      <xs:element name="full_lhs_value" type="xs:int"></xs:element>
+      <xs:element name="full_lhs_value">
+        <xs:complexType>
+          <xs:simpleContent>
+            <xs:extension base="xs:string">
+              <xs:attribute name="binary" type="xs:string"/>
+            </xs:extension>
+          </xs:simpleContent>
+        </xs:complexType>
+      </xs:element>
     </xs:all>
     <xs:attributeGroup ref="traceStepAttrs">
     <xs:attribute name="assignment_type" type="xs:string"></xs:attribute>

doc/assets/xml_spec.xsd

@@ -40,7 +40,15 @@
       <xs:element ref="location" minOccurs="0"/>
       <xs:element name="type" type="xs:string" minOccurs="0"/>
       <xs:element name="full_lhs" type="xs:string"/>
-      <xs:element name="full_lhs_value" type="xs:string"/>
+      <xs:element name="full_lhs_value">
+        <xs:complexType>
+          <xs:simpleContent>
+            <xs:extension base="xs:string">
+              <xs:attribute name="binary" type="xs:string"/>
+            </xs:extension>
+          </xs:simpleContent>
+        </xs:complexType>
+      </xs:element>
     </xs:all>
     <xs:attributeGroup ref="traceStepAttrs"/>
     <xs:attribute name="assignment_type" type="xs:string"/>