diff --git a/doc/assets/README.md b/doc/assets/README.md new file mode 100644 index 00000000000..7addd9399dd --- /dev/null +++ b/doc/assets/README.md @@ -0,0 +1,27 @@ +This folder contains resources for the documentation. + +# XML Spec + +The folllowing files relate to the specification of the XML trace output when using the `--xml-ui` flag. + +## xml_spec.xsd +The`xml_spec.xsd` file is an XSD specification of the trace. You can validate an +output xml file from CBMC using the following invocation: + +```bash +$ cbmc --xml-ui main.c | \ + xmllint --schema xml_spec.xsd --xpath "cprover/result/goto_trace" - +``` + +## xml_spec.tex + +This is a LaTeX document describing the specification of the trace. It can be compiled to pdf using: + +```bash +$ pdflatex -shell-escape xml_spec.tex +``` + +This requires: + + - texlive-latex-base + - texlive-latex-extra (for minted package) diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md index 05df421b0c9..fe3ca41020e 100644 --- a/doc/assets/xml_spec.md +++ b/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 b -1879048192 + ``` **XSD**: @@ -192,7 +200,15 @@ always present - + + + + + + + + + diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex index 8789c58e962..ea78a67e99c 100644 --- a/doc/assets/xml_spec.tex +++ b/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} b -1879048192 + \end{minted} \noindent\textbf{XSD}: @@ -170,7 +183,15 @@ \subsection{Trace Steps in XML} - + + + + + + + + + diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd index 1255c524022..dd3c4b7f11b 100644 --- a/doc/assets/xml_spec.xsd +++ b/doc/assets/xml_spec.xsd @@ -40,7 +40,15 @@ - + + + + + + + + + diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md index 10a6660523d..2c1ab33510d 100644 --- a/doc/cprover-manual/cbmc-tutorial.md +++ b/doc/cprover-manual/cbmc-tutorial.md @@ -138,9 +138,11 @@ possible output format. ``` The specification of the XML trace output can be found here: [XML -Specification](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/assets/xml_spec.tex) -and can be build by `pdflatex -shell-escape xml_spec.tex`. Alternatively, you -view it in Markdown [here](../../../assets/xml_spec). +Specification](../assets/xml_spec.tex) +and can be built by `pdflatex -shell-escape xml_spec.tex`. See the [README +](../assets/README.md#xml_spec.tex) for details. + +Alternatively, you can view it in [Markdown](../assets/xml_spec.md). ### Verifying Modules @@ -348,4 +350,3 @@ comes with a small set of definitions, which includes functions such as We also have a [list of interesting applications of CBMC](http://www.cprover.org/cbmc/applications/). - diff --git a/regression/cbmc/Float24/test.desc b/regression/cbmc/Float24/test.desc index fbb546488c7..1306f3ad6f5 100644 --- a/regression/cbmc/Float24/test.desc +++ b/regression/cbmc/Float24/test.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -5\.1 +5\.1 -- ^warning: ignoring -5\.1l +5\.1l diff --git a/regression/cbmc/float-trace/test.c b/regression/cbmc/float-trace/test.c new file mode 100644 index 00000000000..1f09d8b3ab4 --- /dev/null +++ b/regression/cbmc/float-trace/test.c @@ -0,0 +1,28 @@ +#include +#include +#include + +int main() +{ + float fzero = 0.0f; + float fone = 1.0f; + float fcomplex = 0x1p+37f; + float finf = INFINITY; + float fnan = NAN; + + double dzero = 0.0; + double done = 1.0; + double dinf = INFINITY; + double dnan = NAN; + double dcomplex = -5.56268e-309; + + assert(false); + + return 0; +} + +void test(float value) +{ + assert(value == 1.0f); + assert(value == 0.0f); +} diff --git a/regression/cbmc/float-trace/test.desc b/regression/cbmc/float-trace/test.desc new file mode 100644 index 00000000000..acfd2834cca --- /dev/null +++ b/regression/cbmc/float-trace/test.desc @@ -0,0 +1,32 @@ +CORE +test.c +--trace --xml-ui +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +fzero +0.0f +fone +1.0f +fcomplex +1\.374390e\+11f +finf +\+INFINITY +fnan +\+NAN +\+NAN +dzero +0.0 +done +1.0 +dcomplex +-5\.562680e-309 +finf +\+INFINITY +fnan +\+NAN +\+NAN +-- +-- +Checks that the binary value is printed for floating point types +point types diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 9051ee5230c..caf41b1c83d 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -19,10 +19,38 @@ Author: Daniel Kroening #include #include +#include #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(step.full_lhs_value.type()); +} + +xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) +{ + xmlt full_lhs_value{"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)) + { + 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; +} + void convert( const namespacet &ns, const goto_tracet &goto_trace, @@ -88,16 +116,13 @@ void convert( } } - std::string full_lhs_string, full_lhs_value_string; + std::string full_lhs_string; if(step.full_lhs.is_not_nil()) full_lhs_string = from_expr(ns, identifier, step.full_lhs); - if(step.full_lhs_value.is_not_nil()) - full_lhs_value_string = from_expr(ns, identifier, step.full_lhs_value); - xml_assignment.new_element("full_lhs").data = full_lhs_string; - xml_assignment.new_element("full_lhs_value").data = full_lhs_value_string; + xml_assignment.new_element(full_lhs_value(step, ns)); xml_assignment.set_attribute_bool("hidden", step.hidden); xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));