mirror of
https://github.com/FreeRTOS/coreMQTT
synced 2025-05-14 06:10:09 +08:00

Description ----------- With CBMC v6, unwinding assertions are enabled by default, and object bits no longer need to be set at compile time. Update various build rules to use the latest template as provided with CBMC starter kit. Test Steps ----------- Tested in CI. Checklist: ---------- <!--- Go over all the following points, and put an `x` in all the boxes that apply. --> <!--- If you're unsure about any of these, don't hesitate to ask. We're here to help! --> - [ ] I have tested my changes. No regression in existing tests. - n/a I have modified and/or added unit-tests to cover the code changes in this Pull Request. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
MQTT_ProcessLoop proof
This directory contains a memory safety proof for MQTT_ProcessLoop.
To run the proof.
- Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer to your path.
- Run "make".
- Open html/index.html in a web browser.