len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-16 17:57:44 -04:00
Code Issues Projects Releases Packages Wiki Activity

Update single core CMBC and unit test (#1045)

Browse source 
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.
This commit is contained in:
chinglee-iot 2023-07-24 18:12:20 +08:00 • committed by GitHub
parent 278e6c4b49
commit 7adb08eff5
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
8 changed files with 99 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

14
FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch
View file

@ -1,22 +1,22 @@
diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
index 17a6964e..60ea3e69 100644
index e87db0f45..98f77012f 100644
--- a/FreeRTOS/Source/queue.c
+++ b/FreeRTOS/Source/queue.c
@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t;
@@ -177,7 +177,7 @@ typedef xQUEUE Queue_t;
* to indicate that a task may require unblocking. When the queue in unlocked
* these lock counts are inspected, and the appropriate action taken.
*/
-static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
+void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
/*
* Uses a critical section to determine if there is any data in a queue.
@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer
@@ -2367,7 +2367,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue,
}
/*-----------------------------------------------------------*/
-static void prvUnlockQueue( Queue_t * const pxQueue )
+void prvUnlockQueue( Queue_t * const pxQueue )
{
/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */