cbmc-starter-kit
cbmc-starter-kit copied to clipboard
model-checking
The CBMC stater kit makes it easy to add CBMC verification to a software project.
The step `install latest CBMC` in `aws-c-common`'s `run_cbmc_proofs` CI workflow seems to be failing sporadically. Sometimes the failure disappears when the CI job is re-run but sometimes the failure does...
I have a translation unit in f.h and f.c, all set up for proof using contracts and the starter kit. f.c contains a static (file scope) function that I want...
I am trying to use the starter kit with CBMC 5.84 to verify a few simple functions, but using the function contracts, DFCC, and loop invariant support that was recently...
One user reporter the following error while trying to run the `run-cbmc-proofs.py` script. ```shell ./run-cbmc-proofs.py --proofs aws_byte_buf_append_and_update For your convenience, the output of this run will be symbolically linked to...
- [x] https://github.com/FreeRTOS/CI-CD-Github-Actions/pull/58 then - [x] https://github.com/aws/Device-Defender-for-AWS-IoT-embedded-sdk/pull/70 ([successful run](https://github.com/aws/Device-Defender-for-AWS-IoT-embedded-sdk/actions/runs/4297908877/jobs/7491448292)) - [x] https://github.com/aws/Device-Shadow-for-AWS-IoT-embedded-sdk/pull/113 ([successful run](https://github.com/aws/Device-Shadow-for-AWS-IoT-embedded-sdk/actions/runs/4297909488/jobs/7491449069)) - [x] https://github.com/FreeRTOS/coreMQTT/pull/241 ([successful run](https://github.com/FreeRTOS/coreMQTT/actions/runs/4298053863/jobs/7491739162)) - [x] https://github.com/aws/SigV4-for-AWS-IoT-embedded-sdk/pull/78 ([successful run](https://github.com/aws/SigV4-for-AWS-IoT-embedded-sdk/actions/runs/4298084313/jobs/7491805078)) - [x] https://github.com/FreeRTOS/coreSNTP/pull/71 ([successful run](https://github.com/FreeRTOS/coreSNTP/actions/runs/4297989163/jobs/7491608666)) -...
- [ ] https://github.com/FreeRTOS/CI-CD-Github-Actions/pull/58
When I opened this [PR](https://github.com/model-checking/cbmc-starter-kit/pull/161), @feliperodri informed me that the _Test CBMC starter-kit by using coreHTTP / Python 3.X (pull_request)_ checks had failed. The failure occurred inside of the `jq`...
Documentation should automatically be rebuilt whenever a new version of the CBMC starter kit has been released.
Metadata
Owner
Metadata
The CBMC stater kit makes it easy to add CBMC verification to a software project.