len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-16 01:37:45 -04:00
Code Issues Projects Releases Packages Wiki Activity

Update kernel submodule pointer to version 47338393f (#456)

Browse source 
* Update kernel submodule pointer to version 47338393f

* Fix patches.

Co-authored-by: Carl Lundin <lundinc@amazon.com>
This commit is contained in:
Cobus van Eeden 2020-12-08 15:44:14 -08:00 • committed by GitHub
parent 492ac6edb2
commit c6f4284b76
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 14 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

2
FreeRTOS/Source

@ -1 +1 @@
Subproject commit 50a23218381574f2ba314109691e1de4f8456684
Subproject commit 47338393f1f79558f6144213409f09f81d7c4837

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

@ -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

13
FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch Normal file
View file

@ -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 );