From 584517d467566e5a6e0b6832a6846452bfbecfb1 Mon Sep 17 00:00:00 2001 From: Ravishankar Bhagavandas Date: Tue, 1 Sep 2020 09:26:25 -0700 Subject: [PATCH] cbmc: Add patch to remove overflow assert (#232) --- ...flow-assert-from-xQueueGenericCreate.patch | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch diff --git a/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch new file mode 100644 index 0000000000..6acf1c89a6 --- /dev/null +++ b/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