Skip to content

Commit d744e2d

Browse files
committed
Document the additional binary in the xml file
Because the PR checklist says that feature changes should be documented.
1 parent a1eeb59 commit d744e2d

File tree

2 files changed

+10
-6
lines changed

2 files changed

+10
-6
lines changed

doc/assets/xml_spec.md

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -169,8 +169,10 @@ always present
169169
- `full_lhs`: original lhs expression (after dereferencing)
170170

171171
- `full_lhs_value`: a constant with the new value.
172-
- if the type is a floating point number type, there will be an attribute`binary`
173-
showing its value.
172+
- If the type of data can be represented as a fixed width sequence of bits
173+
then, there will be an attribute `binary` containing the binary
174+
representation. If the data type is signed and the value is negative
175+
then the binary will be encoded using two's complement.
174176

175177
**Example**:
176178

@@ -181,7 +183,7 @@ always present
181183
<location .. />
182184
<type>signed int</type>
183185
<full_lhs>b</full_lhs>
184-
<full_lhs_value>-1879048192</full_lhs_value>
186+
<full_lhs_value binary="10010000000000000000000000000000">-1879048192</full_lhs_value>
185187
</assignment>
186188
<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">
187189
<location file="main.i" function="main" line="3" working-directory="/home/tkiley/workspace/cbmc/regression/cbmc/Float24"/>

doc/assets/xml_spec.tex

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -149,8 +149,10 @@ \subsection{Trace Steps in XML}
149149
\item \texttt{full\_lhs}: original lhs expression (after dereferencing)
150150
\item \texttt{full\_lhs\_value}: a constant with the new value.
151151
\begin{itemize}
152-
\item if the type is a floating point number type, there will be an attribute
153-
\texttt{binary} showing its value.
152+
\item If the type of data can be represented as a fixed width sequence of bits
153+
then, there will be an attribute \texttt{`binary`} containing the binary
154+
representation. If the data type is signed and the value is negative
155+
then the binary will be encoded using two's complement.
154156
\end{itemize}
155157
156158
\end{itemize}
@@ -164,7 +166,7 @@ \subsection{Trace Steps in XML}
164166
<location .. />
165167
<type>signed int</type>
166168
<full_lhs>b</full_lhs>
167-
<full_lhs_value>-1879048192</full_lhs_value>
169+
<full_lhs_value binary="10010000000000000000000000000000">-1879048192</full_lhs_value>
168170
</assignment>
169171
<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">
170172
<location ../>

0 commit comments

Comments
 (0)