From cf39a90d6db3bbd938a1318ff6a90412bcdbd026 Mon Sep 17 00:00:00 2001
From: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Sat, 12 Dec 2020 21:00:03 -0800
Subject: [PATCH] Fix CBMC patches. (#471)

* Fix CBMC patches.
---
 ...emove-static-from-prvCopyDataToQueue.patch | 19 +++++++++----------
 ...low-asserts-from-xQueueGenericCreate.patch |  6 +++---
 .../Task/TaskResumeAll/Configurations.json    | 11 -----------
 3 files changed, 12 insertions(+), 24 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 e081f47252..b72c91a0b0 100644
--- a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
+++ b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
@@ -1,8 +1,8 @@
 diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index edd08b26e..8fa137c9b 100644
+index d2e27e55a..4b05e3c01 100644
 --- a/FreeRTOS/Source/queue.c
 +++ b/FreeRTOS/Source/queue.c
-@@ -191,7 +191,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION;
+@@ -191,14 +191,14 @@ 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.
   */
@@ -11,12 +11,11 @@ index edd08b26e..8fa137c9b 100644
                                        const void * pvItemToQueue,
                                        const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
  
-@@ -2120,7 +2120,7 @@ void vQueueDelete( QueueHandle_t xQueue )
- #endif /* configUSE_MUTEXES */
- /*-----------------------------------------------------------*/
+ /*
+  * Copies an item out of a queue.
+  */
+-static void prvCopyDataFromQueue( Queue_t * const pxQueue,
++void prvCopyDataFromQueue( Queue_t * const pxQueue,
+                                   void * const pvBuffer ) PRIVILEGED_FUNCTION;
  
--static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
-+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
-                                       const void * pvItemToQueue,
-                                       const BaseType_t xPosition )
- {
+ #if ( configUSE_QUEUE_SETS == 1 )
diff --git a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch
index 5665447062..cfd0ac9168 100644
--- a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch
+++ b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch
@@ -1,5 +1,5 @@
 diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index b01dfd11f..b219b599a 100644
+index d2e27e55a..4dd164da6 100644
 --- a/FreeRTOS/Source/queue.c
 +++ b/FreeRTOS/Source/queue.c
 @@ -395,7 +395,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
@@ -9,5 +9,5 @@ index b01dfd11f..b219b599a 100644
 -        configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
 +        /* configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); */
  
-         /* Check for addition overflow. */
-         configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) >  xQueueSizeInBytes );
+         /* Allocate the queue and storage area.  Justification for MISRA
+          * deviation as follows:  pvPortMalloc() always ensures returned memory
diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json
index d2d1ab1f39..70deca7786 100644
--- a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json
@@ -17,8 +17,6 @@
 # EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 # MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 # NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
-# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
-# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 # CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 #
@@ -30,15 +28,6 @@
   "ENTRY": "TaskResumeAll",
   "DEF":
   [
-    { "default":
-      [
-        "FREERTOS_MODULE_TEST",
-        "PENDED_TICKS=1",
-        "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'",
-        "configUSE_TRACE_FACILITY=0",
-        "configGENERATE_RUN_TIME_STATS=0"
-      ]
-    },
     { "useTickHook1":
       [
         "FREERTOS_MODULE_TEST",