FreeRTOS-Kernel/FreeRTOS/Test
Paul Bartell d7e5f40885
Clean up CMock makefiles and add coverage filtering (#523)
* Cleanup Makefiles

* Add lcovrc configuration file

* Add CMock test build directory to .gitignore

* Add callgraph.py and filtercov.py scripts

* Cleanup list Makefile and update list_utest.c with coverage tags

* Add information about coverage filtering and running single test cases

* Remove -fprofile-exclude-files for compatibility with older versions of gcc.
Fix line endings (change to unix style)

* Lint callgraph.py and filtercov.py. Print and error when no target functions are defined.

* Indent with spaces when possible

* Replace tabs with spaces and enable .RECIPEPREFIX

* Add fake_port.h and related portmacro.h changes

* Fix list makefile when bin directory is not available

* Clean up grouped rules

* Update makesfile.. Add "two_tests" example dir

* Fix memory checker error

* Move common makefile items to subdir.mk and testdir.mk includes

* Update core_checker.py exclusions

* Remove line from portmacro.h that doesn't match core_checker.py
2021-03-15 17:01:29 -07:00
..
CBMC Add Litani to run CBMC proofs (#501) 2021-02-12 10:21:07 -08:00
CMock Clean up CMock makefiles and add coverage filtering (#523) 2021-03-15 17:01:29 -07:00
litani@3fc5e02bc1 Add Litani to run CBMC proofs (#501) 2021-02-12 10:21:07 -08:00
VeriFast Minor VeriFast proof changes to match V10.4.3 (#519) 2021-02-25 14:00:22 -07:00
README.md Add VeriFast kernel queue proofs (#117) 2020-07-02 12:55:20 -07:00

Testing in FreeRTOS

FreeRTOS kernel consists of common code and porting layer. Extensive static analysis and dynamic analysis are done on both to ensure functional correctness of FreeRTOS kernel.

For more information on FreeRTOS testing please refer to https://www.freertos.org/FreeRTOS-Coding-Standard-and-Style-Guide.html.

Directory structure

This directory is in working progress -- we are migrating scattered test cases to this directory. Here only lists what's currently under this directory.

  • ./CBMC: This directory contains automated proofs of the memory safety of various parts of the FreeRTOS code base.
  • ./VeriFast: This directory contains automated proofs of the functional correctness of various parts of the FreeRTOS code base.