len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-17 02:07:48 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/CBMC
History
Paul Bartell 569c78fd8c
Remove coroutines (#874) 
* Remove co-routine centric CORTEX_LM3S102_Rowley demos.

Remove CORTEX_LM3S102_Rowley Demo2 and Demo3.
Update Demo1 to no longer use coroutines.

* Remove co-routines from MB91460_Softune demo

* FreeRTOS_96348hs_SK16FX100PMC: Remove co-routine usage.

Remove co-routine usage from FreeRTOS_96348hs_SK16FX100PMC demo.

* MB96350_Softune_Dice_Kit: Remove co-routine usage

Remove co-routines usage from MB96350_Softune_Dice_Kit demo

* AVR_Dx_IAR: Remove co-routine usage

* AVR_Dx_Atmel_Studio: Remove co-routine usage

* PIC24_MPLAB: Remove autogenerated files and add to .gitignore

* PIC24_MPLAB: Remove co-routine usage from demo

* AVR_ATMega323_IAR: Remove co-routine usage

* ColdFire_MCF52221_CodeWarrior: Remove coroutine usage

* AVR_ATMega4809_MPLAB.X: Remove co-routine usage

* AVR_ATMega4809_IAR: Remove co-routine usage

* AVR_ATMega4809_Atmel_Studio: Remove coroutine usage

* AVR_ATMega323_WinAVR: Remove coroutine usage

* AVR_Dx_MPLAB.X: Remove coroutine usage

* dsPIC_MPLAB: Remove coroutine usage

* CORTEX_LM3S102_GCC: Remove coroutines and coroutine centric demos

* CORTEX_LM3S102_GCC: Update makefile to discard unused symbols

Allows fitting in the limited ram/flash for this part.

* CORTEX_LM3S316_IAR: Remove coroutines

* Demos: Remove references to crflash.c, crhook.c, crflash.h, crhook.h

* Remove coroutine options from FreeRTOSConfig.h files

* Xilinx: Remove backup file generated by revup utility

* Demos: Remove Coroutine related config items and references

* Format CBMC FreeRTOSConfig.h

* Update URL from aws.amazon.com/freertos to github.com/FreeRTOS

* Fix copyright year and license text

* Fix license text in demo files

* Update header check excluded path list

* Add configBENCHMARK to lexicon
2022-11-22 10:29:53 +05:30
..
cmake Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
include Created a generic portmacro.h file in the CBMC include folder (#847) 2022-09-26 14:43:54 -07:00
patches Remove coroutines (#874) 2022-11-22 10:29:53 +05:30
proofs Created a generic portmacro.h file in the CBMC include folder (#847) 2022-09-26 14:43:54 -07:00
windows Add uncrustify github workflow (#659) 2021-07-22 14:23:48 -07:00
.gitignore Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
README.md Update readme file with latest instructions to run CBMC proofs (#801) 2022-03-03 11:50:35 -08:00

README.md

CBMC Proof Infrastructure

This directory contains automated proofs of the memory safety of various parts of the FreeRTOS codebase. A continuous integration system validates every pull request posted to the repository against these proofs, and developers can also run the proofs on their local machines.

The proofs are checked using the C Bounded Model Checker, an open-source static analysis tool (GitHub repository). This README describes how to run the proofs on your local clone of FreeRTOS.

Building and running proofs

Currently, only python based builds are supported for the CBMC proofs. The proofs can be run on Linux and MacOS. Windows users can use WSL. The below section outlines the instructions for the Python based build.

Prerequisites

On Windows, you can install WSL using these simple instructions.

You will need Python version >= 3.7. And you will need Make to build and run the proofs.

If you are running on a 64-bit machine, please install the 32-bit version of gcc libraires. For example, on linux, one would run the following command to install the libraries: sudo apt-get install gcc-multilib

Installing CBMC

  • The latest installation instructions can be found on the releases page of the CBMC repository.

  • Please follow all the installation instructions given for your platform.

  • Ensure that you can run the programs cbmc, goto-cc (or goto-cl on Windows), and goto-instrument from the command line. If you cannot run these commands, please refer to the above instructions to install CBMC.

Installing CBMC-viewer (to generate the report)

  • The latest installation instructions can be found on the releases page of the CBMC-viewer repository.

  • Please follow all the installation instructions given for your platform.

  • Ensure that you can run the programs cbmc-viewer. If not, please verify that all instructions above have been followed.

Setting up the proofs

Make sure that all the submodules of the FreeRTOS repository have been cloned. To clone all the submodules, go to the root of the FreeRTOS repository and run this command: git submodule update --init --recursive --checkout.

Change into the proofs directory and run

python3 prepare.py

If you are on a Windows machine but want to generate Linux Makefiles (or vice versa), you can pass the --system linux or --system windows options to those programs.

Running the proofs

Each of the leaf directories under proofs is a proof of the memory safety of a single entry point in FreeRTOS. The scripts that you ran in the previous step will have left a Makefile in each of those directories. To run a proof, change into the directory for that proof and run make. The proofs may take some time to run; they eventually write their output to cbmc.txt, which should have the text VERIFICATION SUCCESSFUL at the end.

The make command will also generate a report in html and json format which makes understanding the failures easier.

Proof directory structure

This directory contains the following subdirectories:

  • proofs contains the proofs run against each pull request
  • patches contains a set of patches that get applied to the codebase prior to running the proofs. The patches are used to remove static and volatile qulaifiers from the source.
  • include and windows contain header files used by the proofs.