mirror of
https://github.com/FreeRTOS/coreMQTT
synced 2025-05-13 21:59:40 +08:00
8ec72d6ef7
Description ----------- This PR: Adds CBMC proofs for the new APIs added for publish retransmits in #308 Test Steps ----------- Proofs run without any errors or warnings Checklist: ---------- - [x] I have tested my changes. No regression in existing tests. - [x] I have modified and/or added unit-tests to cover the code changes in this Pull Request. Related Issue ----------- <!-- If any, please provide issue ID. --> By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: DakshitBabbar <dakshba@amazon.com> Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
CBMC proofs
This directory contains the CBMC proofs. Each proof is in its own directory.
This directory includes four Makefiles.
One Makefile describes the basic workflow for building and running proofs:
- Makefile.common:
- make: builds the goto binary, does the cbmc property checking and coverage checking, and builds the final report.
- make goto: builds the goto binary
- make result: does cbmc property checking
- make coverage: does cbmc coverage checking
- make report: builds the final report
Three included Makefiles describe project-specific settings and can override definitions in Makefile.common:
- Makefile-project-defines: definitions like compiler flags required to build the goto binaries, and definitions to override definitions in Makefile.common.
- Makefile-project-targets: other make targets needed for the project
- Makefile-project-testing: other definitions and targets needed for unit testing or continuous integration.