len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-14 08:47:45 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test
History
Carl Lundin aaece95529
Update Tasks.c CBMC Proofs to Latest Code (#547) 
* Fix Tasks.c patch, line numbers were out of sync and patching was
broken.
* Add assumption to TaskCreate proof that a task's priority is less than
the configured max.

With the introduction of
9efe10b805
an assertion is added to ensure a new task's priority is less than the
confirmed max. The CBMC proof for TaskCreate needs to include this assumption
in order to not assert and fail. Since this is now enforced in the code
we can add an assumption to the proof that a task must be created with a
priority smaller than the configured max.
2021-04-02 14:17:26 -07:00
..
CBMC Update Tasks.c CBMC Proofs to Latest Code (#547) 2021-04-02 14:17:26 -07:00
CMock Re-enable list, message_buffer, and stream_buffers unit tests 2021-04-01 10:52:03 -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

README.md

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.