mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-29 00:36:16 -04:00
4a026fd703
* Move forward Kernel submodule pointer * Fixing patches for CBMC proofs * Update proofs to assume cTxLock != 127 * Update proofs to assume cRxLock != 127
76 lines
3.9 KiB
Diff
76 lines
3.9 KiB
Diff
This patch removes the volatile qualifier from some global variable
|
|
declarations in the tasks.c file. For task pool proofs, we are running
|
|
`goto-instrument` with the `--nondet-volatile` flag on, which causes reads from
|
|
volatile variable to be nondeterministic (i.e., any possible value can be
|
|
returned). This is actually the desired behavior for volatile variables
|
|
regarding verification purposes. However, this causes a lot of trouble when
|
|
such variables are pointers, since one of the possible values we can get when
|
|
dereferencing a volatile pointer is `NULL`.
|
|
|
|
In the case of `uxPendedTicks`, a non-volatile copy of the variable is done
|
|
before the following loop in tasks.c (lines 2231-2255):
|
|
|
|
{
|
|
UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */
|
|
|
|
if( uxPendedCounts > ( UBaseType_t ) 0U )
|
|
{
|
|
do
|
|
{
|
|
if( xTaskIncrementTick() != pdFALSE )
|
|
{
|
|
xYieldPending = pdTRUE;
|
|
}
|
|
else
|
|
{
|
|
mtCOVERAGE_TEST_MARKER();
|
|
}
|
|
--uxPendedCounts;
|
|
} while( uxPendedCounts > ( UBaseType_t ) 0U );
|
|
|
|
uxPendedTicks = 0;
|
|
}
|
|
else
|
|
{
|
|
mtCOVERAGE_TEST_MARKER();
|
|
}
|
|
}
|
|
|
|
Here, `uxPendedTicks` could return any value, making it impossible to unwind
|
|
(or unroll) this loop in CBMC. Therefore, we require `uxPendedTicks` to behave
|
|
as a regular variable so that the loop can be unwound.
|
|
|
|
---
|
|
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
|
|
@@ -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. */
|
|
-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
|
|
@@ -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 )
|
|
@@ -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;
|