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

Tox regression testing (simpler implementation) #54

Closed markrtuttle closed 2 years ago

markrtuttle commented 2 years ago

This uses tox (the python regressing testing implementation) to test the packaging and regression tests, which has the option of doing this under many versions of python.

The main regression test is to clone the coreHTTP repository, break the proofs, run all the proofs, and compare the html and json generated to the expected output. There are two scripts compare-result and compare-source to compare the result and source json since they may differ by timestamps and pathnames. Everything else is a straight diff. The expected output is in the expected directory and can be ignored.

The file to focus on is ./tox.ini that defines the tox testing, and also the two compare scripts.

This replaces https://github.com/awslabs/aws-viewer-for-cbmc/pull/6

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

Closing in favor of https://github.com/awslabs/aws-viewer-for-cbmc/pull/55