cbmc: Add patch to remove overflow assert (#232)

FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch

@@ -0,0 +1,20 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index edd08b26e..259c609f4 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -394,8 +394,13 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
+          * zero in the case the queue is used as a semaphore. */
+         xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */
+ 
+-        /* Check for multiplication overflow. */
+-        configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
++        /*
++         * Multiplication overflow check is commented out in CBMC test as it involves an
++         * expensive division operation and consumes longer compute time against a wide
++         * range of input combination in CBMC proof.
++         *
++         * configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
++         */
+ 
+         /* Allocate the queue and storage area.  Justification for MISRA
+          * deviation as follows:  pvPortMalloc() always ensures returned memory