Skip to content

Print binary values of floats #5322

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
May 7, 2020
Merged

Print binary values of floats #5322

Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
226b71b
Add test for printing different float values in the trace
Apr 24, 2020
7e5b37e
Adapt test to check for binary in trace
Apr 24, 2020
9384b91
Add additional tests for more types
Apr 24, 2020
b64757e
Pull out function for producing the full_lhs_value
Apr 24, 2020
e57e194
Tidy up full_lhs_value
May 6, 2020
304c92c
Adapt full_lhs_value to output binary for floating values
Apr 30, 2020
4049f15
Adapt the XSD to include the binary output
Apr 30, 2020
4fcbd37
Add folder readme for doc/assets
Apr 30, 2020
cdb0b78
Referenced readme in cprover docs
Apr 30, 2020
be6f20f
Rename variables in test to avoid clash on windows
May 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions doc/cprover-manual/cbmc-tutorial.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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/).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't there be a newline here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was auto-removed on save, because there are two new lines at the end of the file