diff options
| author | Cobus van Eeden <35851496+cobusve@users.noreply.github.com> | 2020-08-26 13:07:15 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-26 13:07:15 -0700 |
| commit | a691c6199eebd1f8a8c434ac3e658337bfda6bf6 (patch) | |
| tree | 4216987e9ce2c56a161839ef5b1f71ddcf022d15 | |
| parent | 86117b5173dd85e2b037f81a8c8de2439e47306c (diff) | |
| download | freertos-git-a691c6199eebd1f8a8c434ac3e658337bfda6bf6.tar.gz | |
Updating queue.c patches for CBMC proofs (#216)
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch | 26 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0006-Remove-static-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 5a79ae8cd..e081f4725 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 9cbe7cf5f..bcbd2b5cb 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 ) |