len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-23 21:27:45 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate
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
..
Makefile.json 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 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
TaskCreate_harness.c Update Tasks.c CBMC Proofs to Latest Code (#547) 2021-04-02 14:17:26 -07:00
tasks_test_access_functions.h 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

This proof demonstrates the memory safety of the TaskCreate function. We initialize task lists, but we set other data structures to unconstrained (arbitrary) values, including the data structures pxCurrentTCB, uxCurrentNumberOfTasks, pcName and pxCreateTask. STACK_DEPTH is set to a fixed number (10) since it is not possible to specify a range.

This proof is a work-in-progress. Proof assumptions are described in the harness. The proof also assumes the following functions are memory safe and have no side effects relevant to the memory safety of this function:

  • prvTraceGetObjectHandle
  • prvTraceGetTaskNumber
  • prvTraceSetObjectName
  • prvTraceSetPriorityProperty
  • prvTraceStoreKernelCall
  • prvTraceStoreTaskReady
  • pxPortInitialiseStack
  • vPortEnterCritical
  • vPortExitCritical
  • vPortGenerateSimulatedInterrupt