mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-29 00:36:16 -04:00
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. |
||
|---|---|---|
| .. | ||
| .gitattributes | ||
| .gitignore | ||
| 0005-remove-static-from-prvCopyDataToQueue.patch | ||
| 0005-Remove-volatile-qualifier-from-tasks-variables.patch | ||
| 0006-Remove-static-from-prvNotifyQueueSetContainer.patch | ||
| 0007-Remove-static-from-prvUnlockQueue.patch | ||
| 0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch | ||
| __init__.py | ||
| compute_patch.py | ||
| FreeRTOSConfig.h | ||
| FreeRTOSIPConfig.h | ||
| Makefile | ||
| patch.py | ||
| patches_constants.py | ||
| README.md | ||
| unpatch.py | ||
This directory includes patches to FreeRTOS required to run the CBMC proofs.
The patches fall into three classes:
- First is a refactoring of prvCheckOptions
- Second is the removal of static attributes from some functions
- Third is two patches dealing with shortcomings of CBMC that should be removed soon.