Skip to content

Commit bcec1f9

Browse files
angelonakospaulbartell
authored andcommitted
Update README to include a section on CBMC
1 parent d252ffb commit bcec1f9

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

README.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,14 @@ git submodule update --checkout --init --recursive test/unit-test/CMock
115115

116116
1. Run `cd build && ctest` to execute all tests and view the test run summary.
117117

118+
## CBMC
119+
120+
To learn more about CBMC and proofs specifically, review the training material [here](https://model-checking.github.io/cbmc-training).
121+
122+
The `test/cbmc/proofs` directory contains CBMC proofs.
123+
124+
In order to run these proofs you will need to install CBMC and other tools by following the instructions [here](https://model-checking.github.io/cbmc-training/installation.html).
125+
118126
## Reference examples
119127

120128
Please refer to the demos of the Cellular Interface library [here](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Cellular_Interface_Windows_Simulator) using FreeRTOS on the Windows simulator platform. These can be used as reference examples for the library API.

0 commit comments

Comments
 (0)