Add regression testing both for pull requests and for developer use. A preliminary implementation appears in the tests directory that compares the HTTP proofs before and after the configuration change under test.
The tooling branch of the fork https://github.com/markrtuttle/aws-viewer-for-cbmc includes more sophisticated testing to run cbmc in different configurations against any subset of all known CBMC proofs using the starter kit.
Closing as the tests directory now includes regression testing from http and kani, and the http testing does not compare the output of two versions of viewer.
Add regression testing both for pull requests and for developer use. A preliminary implementation appears in the tests directory that compares the HTTP proofs before and after the configuration change under test.
The tooling branch of the fork https://github.com/markrtuttle/aws-viewer-for-cbmc includes more sophisticated testing to run cbmc in different configurations against any subset of all known CBMC proofs using the starter kit.