search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Refactor result parsing #64

Closed markrtuttle closed 2 years ago

markrtuttle commented 2 years ago

The prior version of the result parsing (especially the text parsing) involved large loops that were hard to understand. This commit refactors the code into small methods to parse for the program version, to parse for status messages, to parse for warnings, etc. The result makes it easier to read, but also makes it easier to see that the text, json, and xml parsing are producing the same results.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

markrtuttle commented 2 years ago

In the coreHTTP regression tests --- to appear soon --- I break the proofs. So there are failures all over the place. But the regressions you propose are also in the works.