FreeRTOS-Kernel/FreeRTOS/Test
Paul Bartell 570ae6bb52
Add unity memory extension, fake_assert, and enable -fsanitize=address (#506)
* Enable libunitymemory extension to track dynamic memory usage during unit tests
* Use UnityMemory in timers_utest.c
* Add fake_assert.h to allow mocking of configASSERT calls
* Add .editorconfig to make github show indentation correctly
* Add unity memory and fake_assert to queue_utest.c
* Add -fsanitize=address CFLAG when running unit tests
* Define mtCOVERAGE_TEST_MARKER macro to include mtCOVERAGE_TEST_MARKER lines in coverage figures
* Add additional memory check / protection CFLAGS for CMock tests
* Fix out of bounds array access in list_utest.c
* Move the fake_assert.h include to the top of FreeRTOSConfig.h
2021-02-18 10:15:01 -08:00
..
CBMC Add Litani to run CBMC proofs (#501) 2021-02-12 10:21:07 -08:00
CMock Add unity memory extension, fake_assert, and enable -fsanitize=address (#506) 2021-02-18 10:15:01 -08:00
litani@3fc5e02bc1 Add Litani to run CBMC proofs (#501) 2021-02-12 10:21:07 -08:00
VeriFast [AUTO][RELEASE]: Bump file header version to "202012.00" 2020-12-15 11:50:37 -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.