len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-15 09:17:44 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll
History
Carl Lundin cf39a90d6d
Fix CBMC patches. (#471) 
* Fix CBMC patches.
2020-12-12 21:00:03 -08:00
..
Configurations.json Fix CBMC patches. (#471) 2020-12-12 21:00:03 -08: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
TaskResumeAll_harness.c 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
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 TaskResumeAll function. We assume that task lists are initialized and filled with a few list items. We also assume that some global variables are set to a nondeterministic value, except for uxSchedulerSuspended which cannot be 0 and xPendedTicks which is either 1 (to unwind a loop in a reasonable amount of time) or 0.

Configurations available:

  • default: The default configuration.
  • useTickHook1: The default configuration with configUSE_TICK_HOOK=1

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:

  • vApplicationTickHook
  • vPortEnterCritical
  • vPortExitCritical
  • vPortGenerateSimulatedInterrupt