diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch index 29cde0e77..7eb4870a0 100644 --- a/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -45,35 +45,32 @@ diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c index ff657733..8b57d198 100644 --- a/FreeRTOS/Source/tasks.c +++ b/FreeRTOS/Source/tasks.c -@@ -331,7 +331,7 @@ typedef tskTCB TCB_t; +@@ -335,7 +335,7 @@ typedef tskTCB TCB_t; /*lint -save -e956 A manual analysis and inspection has been used to determine - which static variables must be declared volatile. */ + * which static variables must be declared volatile. */ -PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; +PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL; /* Lists for ready and blocked tasks. -------------------- - xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but -@@ -340,8 +340,8 @@ the static qualifier. */ - PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */ - PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ - PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ --PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ --PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ -+PRIVILEGED_DATA static List_t * pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ -+PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ - PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ + * xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but +@@ -344,8 +344,8 @@ PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; + PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ]; /*< Prioritised ready tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ +-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ +-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ ++PRIVILEGED_DATA static List_t * pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ ++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ + PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ - #if( INCLUDE_vTaskDelete == 1 ) -@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp - - /* Other file private variables. --------------------------------*/ - PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U; - PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; - PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; - PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; --PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U; -+PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U; - PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE; - PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0; - PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U; + #if ( INCLUDE_vTaskDelete == 1 ) +@@ -372,7 +372,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType + PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; + PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; + PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; +-PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U; ++PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U; + PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE; + PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0; + PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch index 5a79ae8cd..e081f4725 100644 --- a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -1,22 +1,22 @@ diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c -index df2b9c8c..c2265c26 100644 +index edd08b26e..8fa137c9b 100644 --- a/FreeRTOS/Source/queue.c +++ b/FreeRTOS/Source/queue.c -@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION; +@@ -191,7 +191,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION; * Copies an item into the queue, either at the front of the queue or the * back of the queue. */ --static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; -+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; - - /* - * Copies an item out of a queue. -@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue; +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) PRIVILEGED_FUNCTION; + +@@ -2120,7 +2120,7 @@ void vQueueDelete( QueueHandle_t xQueue ) #endif /* configUSE_MUTEXES */ /*-----------------------------------------------------------*/ - --static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) -+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) { - BaseType_t xReturn = pdFALSE; - UBaseType_t uxMessagesWaiting; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch index 9cbe7cf5f..bb8e724d7 100644 --- a/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch +++ b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch @@ -11,12 +11,12 @@ index 17a6964e..24a40c29 100644 #endif /* -@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue; - +@@ -2957,7 +2957,7 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) + #if ( configUSE_QUEUE_SETS == 1 ) - -- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) -+ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) - { - Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer; - BaseType_t xReturn = pdFALSE; + +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) + { + Queue_t * pxQueueSetContainer = pxQueue->pxQueueSetContainer; + BaseType_t xReturn = pdFALSE; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch b/FreeRTOS-Plus/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch new file mode 100644 index 000000000..6acf1c89a --- /dev/null +++ b/FreeRTOS-Plus/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