changes the SPDX identifier in a single CBMC proof's Makefile
introduces updates to the files related to the CBMC starter kit (this was accomplished by running cbmc-starter-kit-update).
removes 2 .git submodules (this was accomplished by running cbmc-starter-kit-update --remove-starter-kit-submodule --remove-litani-submodule). symlinks to files present in the CBMC starter-kit submodule are no longer present Additionally, a user will have to install litani (instructions here) in order to run CBMC proofs locally. litani is present in the CI system that executes the CBMC proofs.
updates the README to include a section on CBMC.
Checklist:
Changes pertain to CBMC proofs, therefore, I perceive the following 2 boxes as not applicable.
[ ] I have tested my changes. No regression in existing tests.
[ ] My code is formatted using Uncrustify.
[x] I have read and applied the rules stated in CONTRIBUTING.md.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Description
This PR:
cbmc-starter-kit-update
).cbmc-starter-kit-update --remove-starter-kit-submodule --remove-litani-submodule
). symlinks to files present in the CBMC starter-kit submodule are no longer present Additionally, a user will have to install litani (instructions here) in order to run CBMC proofs locally. litani is present in the CI system that executes the CBMC proofs.README
to include a section on CBMC.Checklist:
Changes pertain to CBMC proofs, therefore, I perceive the following 2 boxes as not applicable.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.