diff options
| author | Ravishankar Bhagavandas <bhagavar@amazon.com> | 2020-09-01 09:26:25 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-01 09:26:25 -0700 |
| commit | 584517d467566e5a6e0b6832a6846452bfbecfb1 (patch) | |
| tree | 86201f33fa6440e9bd0e4119e2d06328873af9b0 | |
| parent | 18d238ad5cc21ec53008cd21c62c2c10414db3c2 (diff) | |
| download | freertos-git-584517d467566e5a6e0b6832a6846452bfbecfb1.tar.gz | |
cbmc: Add patch to remove overflow assert (#232)
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch | 20 |
1 files changed, 20 insertions, 0 deletions
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 000000000..6acf1c89a --- /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 |