This pull requests updates the CBMC proofs to use the latest versions of the proof starter kit and litani. With these changes, the CBMC proofs are built and checked identically at the command prompt and in continuous integration.
The first five commits in this pull request
Update CBMC litani and starter kit submodules.
Update CBMC proof files from starter kit.
Remove CBMC prepare.py needed only for legacy CI.
Update definitions in CBMC proof Makefiles
Then
One commit updates Makefile-jobs.common to work with the latest version of the starter kit that now depends on litani: it replaces the sed command in Makefile-jobs.common with a litani command invoking sed.
One commit fixes a too-big constant in the Jobs_Describe Makefile that was violating a check in a jobs header file.
There remains one loop-unwinding error in Jobs_Describe to discuss.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
This pull requests updates the CBMC proofs to use the latest versions of the proof starter kit and litani. With these changes, the CBMC proofs are built and checked identically at the command prompt and in continuous integration.
The first five commits in this pull request
Then
There remains one loop-unwinding error in Jobs_Describe to discuss.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.