-
Notifications
You must be signed in to change notification settings - Fork 159
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
e0fc397
commit d60fd28
Showing
1 changed file
with
22 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,22 @@ | ||
This directory contains the proofs checked by CBMC. For each entry point of FreeRTOS tested, there is a directory that contains the test harness and cbmc configuration information needed to check the proof. | ||
This directory contains the proofs checked by CBMC. For each entry point of FreeRTOS-Plus-TCP tested, there is a directory that contains the test harness and cbmc configuration information needed to check the proof. | ||
|
||
### To run the proofs yourselves | ||
|
||
#### Install CBMC | ||
- Install CBMC using the instruction found on the [diffblue github](https://github.com/diffblue/cbmc). | ||
- FOR UBUNTU, you can download the source from the [diffblue github](https://github.com/diffblue/cbmc) and run the below commands: | ||
- After going into the downloaded/cloned repo directory, run `make -C src minisat2-download`. | ||
- Run `make -C src -j8 CXX=g++-6` | ||
|
||
#### Download the FreeRTOS-Plus-TCP repository | ||
- See the instructions for cloning this repository in the [README.md](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP#cloning-this-repository). | ||
|
||
#### Prepare the proofs | ||
- Go to the `test/cbmc/proofs` directory (most probably you are in this directory right now). | ||
- Run `python3 prepare.py`. Note: It is important that you use `python3`. | ||
|
||
#### Run the proofs | ||
- Select a proof to run. We shall choose `ARP/ARPAgeCache` as an example. | ||
- Go to the proof directory (`ARP/ARPAgeCache`). | ||
- Run `make cbmc`. | ||
- Run `make report`. This command should generate an HTML file which can be opened in a web-browser and can be traversed like a web page. |