From a691c6199eebd1f8a8c434ac3e658337bfda6bf6 Mon Sep 17 00:00:00 2001 From: Cobus van Eeden <35851496+cobusve@users.noreply.github.com> Date: Wed, 26 Aug 2020 13:07:15 -0700 Subject: [PATCH] Updating queue.c patches for CBMC proofs (#216) --- ...emove-static-from-prvCopyDataToQueue.patch | 26 +++++++++---------- ...atic-from-prvNotifyQueueSetContainer.patch | 2 +- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch index 5a79ae8cd4..e081f47252 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -1,22 +1,22 @@ diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c -index df2b9c8c..c2265c26 100644 +index edd08b26e..8fa137c9b 100644 --- a/FreeRTOS/Source/queue.c +++ b/FreeRTOS/Source/queue.c -@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION; +@@ -191,7 +191,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION; * Copies an item into the queue, either at the front of the queue or the * back of the queue. */ --static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; -+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; - - /* - * Copies an item out of a queue. -@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue; +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) PRIVILEGED_FUNCTION; + +@@ -2120,7 +2120,7 @@ void vQueueDelete( QueueHandle_t xQueue ) #endif /* configUSE_MUTEXES */ /*-----------------------------------------------------------*/ - --static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) -+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) { - BaseType_t xReturn = pdFALSE; - UBaseType_t uxMessagesWaiting; diff --git a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch index 9cbe7cf5f7..bcbd2b5cbd 100644 --- a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch +++ b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch @@ -11,7 +11,7 @@ index 17a6964e..24a40c29 100644 #endif /* -@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue; +@@ -2957,7 +2957,7 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) #if ( configUSE_QUEUE_SETS == 1 )