len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-16 09:47:44 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick
History
chinglee-iot 7adb08eff5
Update single core CMBC and unit test (#1045) 
This PR fixes CBMC and unit test for single core FreeRTOS in the FreeRTOS-Kernel PR - https://github.com/FreeRTOS/FreeRTOS-Kernel/pull/716.

- xYieldPendings and xIdleTaskHandles are now an array. Update in FreeRTOS unit test.
-  Update CBMC patches.
2023-07-24 15:42:20 +05:30
..
cbmc-viewer.json Add CBMC viewer configuration files (#683) 2021-09-13 21:23:35 -04:00
Configurations.json Update submodule pointer for Kernel V10.6.0 (#1037) 2023-07-18 09:28:02 +05:30
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
TaskIncrementTick_harness.c Apply release changes to main branch (#759) 2021-12-23 10:16:27 -08:00
tasks_test_access_functions.h Update single core CMBC and unit test (#1045) 2023-07-24 15:42:20 +05:30

README.md

This proof demonstrates the memory safety of the TaskIncrementTick function. We assume that task lists are initialized and filled with a few list items. We also assign nondeterministic values to some global variables.

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:

  • prvTraceGetTaskNumber
  • prvTracePortGetTimeStamp
  • prvTraceStoreKernelCallWithNumericParamOnly
  • prvTraceStoreTaskReady
  • vApplicationTickHook