From c6f4284b760f7698febb04fb5ce8fb5b802f5fdf Mon Sep 17 00:00:00 2001 From: Cobus van Eeden <35851496+cobusve@users.noreply.github.com> Date: Tue, 8 Dec 2020 15:44:14 -0800 Subject: [PATCH] Update kernel submodule pointer to version 47338393f (#456) * Update kernel submodule pointer to version 47338393f * Fix patches. Co-authored-by: Carl Lundin --- FreeRTOS/Source | 2 +- ...flow-assert-from-xQueueGenericCreate.patch | 20 ------------------- ...low-asserts-from-xQueueGenericCreate.patch | 13 ++++++++++++ 3 files changed, 14 insertions(+), 21 deletions(-) delete mode 100644 FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch create mode 100644 FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch diff --git a/FreeRTOS/Source b/FreeRTOS/Source index 50a2321838..47338393f1 160000 --- a/FreeRTOS/Source +++ b/FreeRTOS/Source @@ -1 +1 @@ -Subproject commit 50a23218381574f2ba314109691e1de4f8456684 +Subproject commit 47338393f1f79558f6144213409f09f81d7c4837 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 deleted file mode 100644 index 6acf1c89a6..0000000000 --- a/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch +++ /dev/null @@ -1,20 +0,0 @@ -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 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 new file mode 100644 index 0000000000..5665447062 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch @@ -0,0 +1,13 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index b01dfd11f..b219b599a 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -395,7 +395,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue, + 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 ) ) ); ++ /* configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); */ + + /* Check for addition overflow. */ + configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) > xQueueSizeInBytes );