mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-18 10:47:47 -04:00
20 lines
1.1 KiB
Diff
20 lines
1.1 KiB
Diff
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
|