Add XML trace specification -- no code change #5222

xbauch · 2020-01-31T16:30:38Z

and a reference in the documentation.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

hannes-steffenhagen-diffblue · 2020-01-31T16:49:57Z

doc/cprover-manual/cbmc-tutorial.md

+```
+
+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)


This should contain information on how the file is intended to be processed. I think this should work with most LaTeX backends with -shell-escape?

Also, maybe even consider producing it as part of our documentation somehow? The LaTeX itself isn’t super human readable unprocessed.

Yeah 🚫 there must be either a script or a readme next to it explaining how to build it.

majakusber · 2020-01-31T17:44:55Z

Codecov Report

Merging #5222 into develop will not change coverage by %.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5222   +/-   ##
========================================
  Coverage    67.43%   67.43%           
========================================
  Files         1157     1157           
  Lines        95351    95351           
========================================
  Hits         64303    64303           
  Misses       31048    31048

Flag	Coverage Δ
#cproversmt2	`42.67% <ø> (ø)`	⬆️
#regression	`63.96% <ø> (ø)`	⬆️
#unit	`31.95% <ø> (ø)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 5b4bcc6...e6c2933. Read the comment docs.

majakusber · 2020-02-05T14:50:44Z

Why is my face on the codecov comment? 👀

xbauch · 2020-02-05T14:58:36Z

Why is my face on the codecov comment?

Wait. You didn't post the coverage report here?

majakusber · 2020-02-05T15:08:37Z

Nope, never seen this PR, never did anything with codecov 🤷‍♀️ I only learned about this because I got emails from github after Thomas added his comment (but not earlier).

martin-cs

I appreciate that documentation is often a thankless task so forgive me if I am making this harder but would it be possible to produce the spec as an XSD file or something so that we add a regression test that validates the output of CBMC against it. That way when someone changes the format we should at least have a flag to update the documentation.

and a reference in the documentation.

Also replace some latex instructions that pandoc can’t handle with some it can.

Note that this is based on observed outputs from cbmc, there is currently no mechanism in place that enforces CBMC to conform to this. We have discussed adding a regression test pass for checking that at least our own regression tests conform to the spec. In a future PR.

codecov-io · 2020-02-25T14:43:13Z

Codecov Report

Merging #5222 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5222   +/-   ##
========================================
  Coverage    67.42%   67.42%           
========================================
  Files         1162     1162           
  Lines        95620    95620           
========================================
  Hits         64476    64476           
  Misses       31144    31144

Flag	Coverage Δ
#cproversmt2	`100% <ø> (+57.4%)`	⬆️
#regression	`63.95% <ø> (ø)`	⬆️
#unit	`31.89% <ø> (ø)`	⬆️

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_dec.h	`100% <0%> (ø)`	⬆️
src/solvers/smt2/letify.cpp	`100% <0%> (ø)`	⬆️
src/solvers/floatbv/float_bv.h	`100% <0%> (ø)`	⬆️
src/solvers/smt2/smt2irep.cpp	`88% <0%> (ø)`	⬆️
src/solvers/floatbv/float_bv.cpp	`74.36% <0%> (ø)`	⬆️
src/solvers/smt2/smt2_dec.cpp	`67.69% <0%> (ø)`	⬆️
src/solvers/smt2/letify.h	`100% <0%> (ø)`	⬆️
src/solvers/smt2/smt2_conv.h	`100% <0%> (ø)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`57.23% <0%> (ø)`	⬆️
src/solvers/flattening/pointer_logic.cpp	`89.39% <0%> (ø)`	⬆️
... and 17 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1f2f1fa...44879df. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-03-02T15:56:46Z

Turning it off and turning it on again

thk123 · 2020-03-03T10:13:20Z

doc/cprover-manual/cbmc-tutorial.md

+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).


This link doesn't seem to work, I think you only need to go up two directories

Suggested change

view it in Markdown [here](../../../assets/xml_spec).

view it in Markdown [here](../../assets/xml_spec).

The link doesn’t work because it links to the develop documentation, which doesn’t have this yet I think.

chrisr-diffblue

This looks like a great improvement.

xbauch requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners January 31, 2020 16:30

hannes-steffenhagen-diffblue reviewed Jan 31, 2020

View reviewed changes

xbauch force-pushed the feature/xml-spec branch from e6c2933 to b4c30fe Compare February 6, 2020 10:57

martin-cs approved these changes Feb 6, 2020

View reviewed changes

xbauch force-pushed the feature/xml-spec branch 2 times, most recently from 6b53770 to 1bd6f05 Compare February 7, 2020 12:41

petr-bauch and others added 2 commits February 24, 2020 17:21

Add XML trace specification

39b2b12

and a reference in the documentation.

Fix some typos/syntax errors in xml_spec.tex

7e2ad38

Also replace some latex instructions that pandoc can’t handle with some it can.

xbauch force-pushed the feature/xml-spec branch from 1bd6f05 to 54a208f Compare February 24, 2020 17:22

xbauch added the do not merge label Feb 25, 2020

xbauch force-pushed the feature/xml-spec branch from f2a95f4 to 44879df Compare February 25, 2020 14:39

xbauch removed the do not merge label Feb 25, 2020

hannes-steffenhagen-diffblue closed this Mar 2, 2020

hannes-steffenhagen-diffblue reopened this Mar 2, 2020

thk123 reviewed Mar 3, 2020

View reviewed changes

chrisr-diffblue approved these changes Mar 3, 2020

View reviewed changes

hannes-steffenhagen-diffblue merged commit 8db2b8b into diffblue:develop Mar 4, 2020

	view it in Markdown [here](../../../assets/xml_spec).
	view it in Markdown [here](../../assets/xml_spec).

Add XML trace specification -- no code change #5222

Add XML trace specification -- no code change #5222

Uh oh!

Conversation

xbauch commented Jan 31, 2020

Uh oh!

hannes-steffenhagen-diffblue Jan 31, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jan 31, 2020

Choose a reason for hiding this comment

Uh oh!

thk123 Feb 5, 2020

Choose a reason for hiding this comment

Uh oh!

majakusber commented Jan 31, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

majakusber commented Feb 5, 2020

Uh oh!

xbauch commented Feb 5, 2020

Uh oh!

majakusber commented Feb 5, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Feb 25, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

hannes-steffenhagen-diffblue commented Mar 2, 2020

Uh oh!

thk123 Mar 3, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Mar 4, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

majakusber commented Jan 31, 2020 •

edited

Loading

codecov-io commented Feb 25, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Mar 4, 2020 •

edited

Loading