len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity

Proved memory safety of name-writing loop in prvInitialiseNewTask.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-25 14:57:26 -04:00
parent 82be7cb23a
commit 8a8f0ab9b1
3 changed files with 124 additions and 102 deletions
Download patch file Download diff file Expand all files Collapse all files

15
tasks.c
View file

@ -1300,7 +1300,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
UBaseType_t uxPriority,
TaskHandle_t * const pxCreatedTask )
/*@ requires usStackDepth * sizeof( StackType_t ) < UINTPTR_MAX &*&
usStackDepth > 0;
usStackDepth > 0 &*&
// We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars(pcName, 16, _);
@*/
//@ ensures true;
#if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) )
@ -1426,7 +1428,9 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
/*@ requires TCB_p(pxNewTCB, ?stackSize) &*&
stackSize == ulStackDepth * sizeof(StackType_t) &*&
stackSize <= UINTPTR_MAX &*&
ulStackDepth > 0;
ulStackDepth > 0 &*&
// We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars(pcName, 16, _);
@*/
/*@ ensures true;
@*/
@ -1524,11 +1528,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
}
#endif /* portSTACK_GROWTH */
//@ close TCB_p(pxNewTCB, stackSize);
/* Store the task name in the TCB. */
if( pcName != NULL )
{
for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) configMAX_TASK_NAME_LEN; x++ )
/*@ invariant TCB_p(pxNewTCB, stackSize) &*&
chars(pcName, 16, _);
@*/
{
//@ open TCB_p(_, _);
pxNewTCB->pcTaskName[ x ] = pcName[ x ];
/* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than
@ -1542,6 +1552,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{
mtCOVERAGE_TEST_MARKER();
}
//@ close TCB_p(_, _);
}
/* Ensure the name string is terminated in the case that the string length

209
verification/verifast/preprocessed_files/tasks--pp.c
View file

@ -99,7 +99,7 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*&
// pcTaskName
// Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars_(tcb->pcTaskName, 16, _) &*&
tcb->uxCriticalNesting |-> _ &*&
@ -10717,10 +10717,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
UBaseType_t uxPriority,
TaskHandle_t * const pxCreatedTask )
/*@ requires usStackDepth * sizeof( StackType_t ) < UINTPTR_MAX &*&
usStackDepth > 0;
usStackDepth > 0 &*&
// We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars(pcName, 16, _);
@*/
//@ ensures true;
// # 1319 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1321 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
TCB_t * pxNewTCB;
BaseType_t xReturn;
@ -10728,7 +10730,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
/* If the stack grows down then allocate the stack then the TCB so the stack
* does not grow into the TCB. Likewise if the stack grows up then allocate
* the TCB then the stack. */
// # 1349 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1351 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
StackType_t * pxStack;
@ -10764,9 +10766,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
if( pxNewTCB != 0 )
{
// # 1392 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1394 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
prvInitialiseNewTask( pxTaskCode, pcName, ( uint32_t ) usStackDepth, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0 );
// # 1401 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1403 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
prvAddNewTaskToReadyList( pxNewTCB );
xReturn = ( ( ( BaseType_t ) 1 ) );
}
@ -10795,14 +10797,16 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
/*@ requires TCB_p(pxNewTCB, ?stackSize) &*&
stackSize == ulStackDepth * sizeof(StackType_t) &*&
stackSize <= UINTPTR_MAX &*&
ulStackDepth > 0;
ulStackDepth > 0 &*&
// We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars(pcName, 16, _);
@*/
/*@ ensures true;
@*/
{
StackType_t * pxTopOfStack;
UBaseType_t x;
// # 1453 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1457 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ open TCB_p(_,_);
/* Avoid dependency on memset() if it is not required. */
@ -10849,14 +10853,20 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
pxTopOfStack = ( StackType_t * ) ( ( ( uint32_t ) pxTopOfStack ) & ( ~( ( uint32_t ) ( 0x0007 ) ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception. Avoiding casts between pointers and integers is not practical. Size differences accounted for using portPOINTER_SIZE_TYPE type. Checked by assert(). */
/* Check the alignment of the calculated top of stack is correct. */
// # 1513 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1517 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
// # 1527 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1531 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ close TCB_p(pxNewTCB, stackSize);
/* Store the task name in the TCB. */
if( pcName != 0 )
{
for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) 16; x++ )
/*@ invariant TCB_p(pxNewTCB, stackSize) &*&
chars(pcName, 16, _);
@*/
{
//@ open TCB_p(_, _);
pxNewTCB->pcTaskName[ x ] = pcName[ x ];
/* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than
@ -10870,6 +10880,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{
;
}
//@ close TCB_p(_, _);
}
/* Ensure the name string is terminated in the case that the string length
@ -10917,7 +10928,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{
pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U;
}
// # 1611 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1622 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
/* Avoid compiler warning about unreferenced parameter. */
( void ) xRegions;
@ -10935,21 +10946,21 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
memset( ( void * ) &( pxNewTCB->ulNotifiedValue[ 0 ] ), 0x00, sizeof( pxNewTCB->ulNotifiedValue ) );
memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) );
}
// # 1640 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1651 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
pxNewTCB->ucDelayAborted = ( ( BaseType_t ) 0 );
}
// # 1658 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1669 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Initialize the TCB stack to look as if the task was already running,
* but had been interrupted by the scheduler. The return address is set
* to the start of the task function. Once the stack has been initialised
* the top of stack variable is updated. */
// # 1686 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
/* If the port has capability to detect stack overflow,
* pass the stack end address to the stack initialization
* function as well. */
// # 1703 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1714 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters );
}
@ -11158,7 +11169,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
if( xTaskRunningOnCore == xCoreID )
{
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1911, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1922, "uxSchedulerSuspended == 0") : (void)0);
vTaskYieldWithinAPI();
}
else
@ -11181,12 +11192,12 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
TickType_t xTimeToWake;
BaseType_t xAlreadyYielded, xShouldDelay = ( ( BaseType_t ) 0 );
(__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1934, "pxPreviousWakeTime") : (void)0);
(__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1935, "( xTimeIncrement > 0U )") : (void)0);
(__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1945, "pxPreviousWakeTime") : (void)0);
(__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1946, "( xTimeIncrement > 0U )") : (void)0);
vTaskSuspendAll();
{
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1939, "uxSchedulerSuspended == 1") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1950, "uxSchedulerSuspended == 1") : (void)0);
/* Minor optimisation. The tick count cannot change in this
* block. */
@ -11272,7 +11283,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
{
vTaskSuspendAll();
{
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2025, "uxSchedulerSuspended == 1") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2036, "uxSchedulerSuspended == 1") : (void)0);
;
/* A task that is removed from the event list while the
@ -11326,7 +11337,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
const TCB_t * const pxTCB = xTask;
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2079, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2090, "pxTCB") : (void)0);
vTaskEnterCritical();
{
@ -11502,7 +11513,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
BaseType_t xYieldForTask = ( ( BaseType_t ) 0 );
BaseType_t xCoreID;
(__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2255, "( uxNewPriority < 32 )") : (void)0);
(__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2266, "( uxNewPriority < 32 )") : (void)0);
/* Ensure the new priority is valid. */
if( uxNewPriority >= ( UBaseType_t ) 32 )
@ -11656,13 +11667,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/*-----------------------------------------------------------*/
// # 2443 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2454 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2466 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2477 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2484 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2495 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2512 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2523 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -11739,7 +11750,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
if( xTaskRunningOnCore == 0 )
{
/* The current task has just been suspended. */
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2588, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2599, "uxSchedulerSuspended == 0") : (void)0);
vTaskYieldWithinAPI();
}
else
@ -11753,7 +11764,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
{
vTaskExitCritical();
(__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2602, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0);
(__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2613, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0);
/* The scheduler is not running, but the task that was pointed
* to by pxCurrentTCB has just been suspended and pxCurrentTCB
@ -11800,7 +11811,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/* Accesses xPendingReadyList so must be called from a critical section. */
/* It does not make sense to check if the calling task is suspended. */
(__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2649, "xTask") : (void)0);
(__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2660, "xTask") : (void)0);
/* Is the task being resumed actually in the suspended list? */
if( ( ( ( &( pxTCB->xStateListItem ) )->pxContainer == ( &xSuspendedTaskList ) ) ? ( ( ( BaseType_t ) 1 ) ) : ( ( ( BaseType_t ) 0 ) ) ) != ( ( BaseType_t ) 0 ) )
@ -11849,7 +11860,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/* It does not make sense to resume the calling task. */
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2698, "xTaskToResume") : (void)0);
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2709, "xTaskToResume") : (void)0);
/* The parameter cannot be NULL as it is impossible to resume the
* currently executing task. It is also impossible to resume a task
@ -11908,7 +11919,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2757, "xTaskToResume") : (void)0);
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2768, "xTaskToResume") : (void)0);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -12029,7 +12040,7 @@ static BaseType_t prvCreateIdleTasks( void )
{
;
}
// # 2925 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2936 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
if( xCoreID == 0 )
{
@ -12041,7 +12052,7 @@ static BaseType_t prvCreateIdleTasks( void )
( ( UBaseType_t ) 0x00 ), /* In effect ( tskIDLE_PRIORITY | portPRIVILEGE_BIT ), but tskIDLE_PRIORITY is zero. */
&xIdleTaskHandle[ xCoreID ] ); /*lint !e961 MISRA exception, justified as it is not a redundant explicit cast to all supported compilers. */
}
// # 2948 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2959 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
@ -12078,7 +12089,7 @@ void vTaskStartScheduler( void )
* so interrupts will automatically get re-enabled when the first task
* starts to run. */
assert_fct(false);
// # 2998 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3009 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL;
xSchedulerRunning = ( ( BaseType_t ) 1 );
xTickCount = ( TickType_t ) 0;
@ -12110,7 +12121,7 @@ void vTaskStartScheduler( void )
/* This line will only be reached if the kernel could not be started,
* because there was not enough FreeRTOS heap to create the idle task
* or the timer task. */
(__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3029, "xReturn != ( -1 )") : (void)0);
(__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3040, "xReturn != ( -1 )") : (void)0);
}
/* Prevent compiler warnings if INCLUDE_xTaskGetIdleTaskHandle is set to 0,
@ -12175,7 +12186,7 @@ void vTaskSuspendAll( void )
}
}
/*----------------------------------------------------------*/
// # 3156 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3167 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
BaseType_t xTaskResumeAll( void )
@ -12198,7 +12209,7 @@ BaseType_t xTaskResumeAll( void )
/* If uxSchedulerSuspended is zero then this function does not match a
* previous call to vTaskSuspendAll(). */
(__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3178, "uxSchedulerSuspended") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3189, "uxSchedulerSuspended") : (void)0);
--uxSchedulerSuspended;
vPortRecursiveLock(1, spin_lock_instance(15), ( ( BaseType_t ) 0 ));
@ -12356,7 +12367,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
/* If null is passed in here then the name of the calling task is being
* queried. */
pxTCB = ( ( ( xTaskToQuery ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToQuery ) );
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3336, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3347, "pxTCB") : (void)0);
return &( pxTCB->pcTaskName[ 0 ] );
}
/*-----------------------------------------------------------*/
@ -12449,7 +12460,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
TCB_t * pxTCB;
/* Task names will be truncated to configMAX_TASK_NAME_LEN - 1 bytes. */
(__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3429, "strlen( pcNameToQuery ) < 16") : (void)0);
(__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3440, "strlen( pcNameToQuery ) < 16") : (void)0);
vTaskSuspendAll();
{
@ -12545,7 +12556,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
* each task in the Suspended state. */
uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended );
}
// # 3539 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3550 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
if( pulTotalRunTime != 0 )
{
@ -12573,7 +12584,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
{
/* If xTaskGetIdleTaskHandle() is called before the scheduler has been
* started, then xIdleTaskHandle will be NULL. */
(__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3566, "( xIdleTaskHandle != 0 )") : (void)0);
(__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3577, "( xIdleTaskHandle != 0 )") : (void)0);
return &( xIdleTaskHandle[ 0 ] );
}
@ -12584,7 +12595,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
* This is to ensure vTaskStepTick() is available when user defined low power mode
* implementations require configUSE_TICKLESS_IDLE to be set to a value other than
* 1. */
// # 3590 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3601 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
@ -12593,7 +12604,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
/* Must not be called with the scheduler suspended as the implementation
* relies on xPendedTicks being wound down to 0 in xTaskResumeAll(). */
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3598, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3609, "uxSchedulerSuspended == 0") : (void)0);
/* Use xPendedTicks to mimic xTicksToCatchUp number of ticks occurring when
* the scheduler is suspended so the ticks are executed in xTaskResumeAll(). */
@ -12612,7 +12623,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
TCB_t * pxTCB = xTask;
BaseType_t xReturn;
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3617, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3628, "pxTCB") : (void)0);
vTaskSuspendAll();
{
@ -12711,7 +12722,7 @@ BaseType_t xTaskIncrementTick( void )
if( xConstTickCount == ( TickType_t ) 0U ) /*lint !e774 'if' does not always evaluate to false as it is looking for an overflow. */
{
{ List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3716, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); };
{ List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3727, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); };
}
else
{
@ -12894,13 +12905,13 @@ BaseType_t xTaskIncrementTick( void )
return xSwitchRequired;
}
/*-----------------------------------------------------------*/
// # 3928 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3939 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 3952 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3963 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 3977 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3988 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 4010 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4021 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
void vTaskSwitchContext( BaseType_t xCoreID )
@ -12918,7 +12929,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
{
/* vTaskSwitchContext() must never be called from within a critical section.
* This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4027, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4038, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
if( uxSchedulerSuspended != ( UBaseType_t ) ( ( BaseType_t ) 0 ) )
{
@ -12930,7 +12941,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
{
xYieldPendings[ xCoreID ] = ( ( BaseType_t ) 0 );
;
// # 4068 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4079 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Check for stack overflow, if configured. */
{ const uint32_t * const pulStack = ( uint32_t * ) xTaskGetCurrentTaskHandle()->pxStack; const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; if( ( pulStack[ 0 ] != ulCheckValue ) || ( pulStack[ 1 ] != ulCheckValue ) || ( pulStack[ 2 ] != ulCheckValue ) || ( pulStack[ 3 ] != ulCheckValue ) ) { vApplicationStackOverflowHook( ( TaskHandle_t ) xTaskGetCurrentTaskHandle(), xTaskGetCurrentTaskHandle()->pcTaskName ); } };
@ -12947,7 +12958,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
;
/* After the new task is switched in, update the global errno. */
// # 4102 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4113 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
vPortRecursiveLock(0, spin_lock_instance(14), ( ( BaseType_t ) 0 ));
@ -12958,7 +12969,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
void vTaskPlaceOnEventList( List_t * const pxEventList,
const TickType_t xTicksToWait )
{
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4112, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4123, "pxEventList") : (void)0);
/* THIS FUNCTION MUST BE CALLED WITH EITHER INTERRUPTS DISABLED OR THE
* SCHEDULER SUSPENDED AND THE QUEUE BEING ACCESSED LOCKED. */
@ -12977,11 +12988,11 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList,
const TickType_t xItemValue,
const TickType_t xTicksToWait )
{
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4131, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4142, "pxEventList") : (void)0);
/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. It is used by
* the event groups implementation. */
(__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4135, "uxSchedulerSuspended != 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4146, "uxSchedulerSuspended != 0") : (void)0);
/* Store the item value in the event list item. It is safe to access the
* event list item here as interrupts won't access the event list item of a
@ -13005,7 +13016,7 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList,
TickType_t xTicksToWait,
const BaseType_t xWaitIndefinitely )
{
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4159, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4170, "pxEventList") : (void)0);
/* This function should not be called by application code hence the
* 'Restricted' in its name. It is not part of the public API. It is
@ -13053,14 +13064,14 @@ BaseType_t xTaskRemoveFromEventList( const List_t * const pxEventList )
* This function assumes that a check has already been made to ensure that
* pxEventList is not empty. */
pxUnblockedTCB = ( ( &( ( pxEventList )->xListEnd ) )->pxNext->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too. Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4207, "pxUnblockedTCB") : (void)0);
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4218, "pxUnblockedTCB") : (void)0);
( void ) uxListRemove( &( pxUnblockedTCB->xEventListItem ) );
if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) )
{
( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) );
; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ;
// # 4228 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4239 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
else
{
@ -13090,7 +13101,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. It is used by
* the event flags implementation. */
(__builtin_expect(!(uxSchedulerSuspended != ( ( BaseType_t ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4257, "uxSchedulerSuspended != ( ( BaseType_t ) 0 )") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended != ( ( BaseType_t ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4268, "uxSchedulerSuspended != ( ( BaseType_t ) 0 )") : (void)0);
/* Store the new item value in the event list. */
( ( pxEventListItem )->xItemValue = ( xItemValue | 0x80000000UL ) );
@ -13098,9 +13109,9 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
/* Remove the event list form the event flag. Interrupts do not access
* event flags. */
pxUnblockedTCB = ( ( pxEventListItem )->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too. Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4265, "pxUnblockedTCB") : (void)0);
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4276, "pxUnblockedTCB") : (void)0);
( void ) uxListRemove( pxEventListItem );
// # 4282 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4293 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Remove the task from the delayed list and add it to the ready list. The
* scheduler is suspended so interrupts will not be accessing the ready
* lists. */
@ -13119,7 +13130,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut )
{
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4300, "pxTimeOut") : (void)0);
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4311, "pxTimeOut") : (void)0);
vTaskEnterCritical();
{
pxTimeOut->xOverflowCount = xNumOfOverflows;
@ -13142,8 +13153,8 @@ BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
{
BaseType_t xReturn;
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4323, "pxTimeOut") : (void)0);
(__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4324, "pxTicksToWait") : (void)0);
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4334, "pxTimeOut") : (void)0);
(__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4335, "pxTicksToWait") : (void)0);
vTaskEnterCritical();
{
@ -13265,7 +13276,7 @@ void vTaskMissedYield( void )
*
* @todo additional conditional compiles to remove this function.
*/
// # 4506 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4517 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*
* -----------------------------------------------------------
* The Idle task.
@ -13295,7 +13306,7 @@ static void prvIdleTask( void * pvParameters )
/* See if any tasks have deleted themselves - if so then the idle task
* is responsible for freeing the deleted task's TCB and stack. */
prvCheckTasksWaitingTermination();
// # 4547 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4558 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
/* When using preemption tasks of equal priority will be
* timesliced. If a task that is sharing the idle priority is ready
@ -13316,16 +13327,16 @@ static void prvIdleTask( void * pvParameters )
;
}
}
// # 4583 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4594 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* This conditional compilation should use inequality to 0, not equality
* to 1. This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when
* user defined low power mode implementations require
* configUSE_TICKLESS_IDLE to be set to a value other than 1. */
// # 4648 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4659 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
/*-----------------------------------------------------------*/
// # 4698 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4709 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -13339,7 +13350,7 @@ static void prvIdleTask( void * pvParameters )
if( xIndex < 5 )
{
pxTCB = ( ( ( xTaskToSet ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToSet ) );
(__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4711, "pxTCB != 0") : (void)0);
(__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4722, "pxTCB != 0") : (void)0);
pxTCB->pvThreadLocalStoragePointers[ xIndex ] = pvValue;
}
}
@ -13370,7 +13381,7 @@ static void prvIdleTask( void * pvParameters )
/*-----------------------------------------------------------*/
// # 4758 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4769 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
static void prvInitialiseTaskLists( void )
@ -13472,7 +13483,7 @@ static void prvCheckTasksWaitingTermination( void )
{
pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority;
}
// # 4870 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4881 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
pxTaskStatus->ulRunTimeCounter = 0;
}
@ -13603,7 +13614,7 @@ static void prvCheckTasksWaitingTermination( void )
/*-----------------------------------------------------------*/
// # 5039 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5050 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -13660,7 +13671,7 @@ static void prvCheckTasksWaitingTermination( void )
free( (void*) pxTCB->pxStack);
free( (void*) pxTCB);
}
// # 5122 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5133 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
@ -13865,8 +13876,8 @@ static void prvResetNextTaskUnblockTime( void )
* If the mutex is held by a task then it cannot be given from an
* interrupt, and if a mutex is given by the holding task then it must
* be the running state task. */
(__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5326, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0);
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5327, "pxTCB->uxMutexesHeld") : (void)0);
(__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5337, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0);
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5338, "pxTCB->uxMutexesHeld") : (void)0);
( pxTCB->uxMutexesHeld )--;
/* Has the holder of the mutex inherited the priority of another
@ -13952,7 +13963,7 @@ static void prvResetNextTaskUnblockTime( void )
{
/* If pxMutexHolder is not NULL then the holder must hold at least
* one mutex. */
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5413, "pxTCB->uxMutexesHeld") : (void)0);
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5424, "pxTCB->uxMutexesHeld") : (void)0);
/* Determine the priority to which the priority of the task that
* holds the mutex should be set. This will be the greater of the
@ -13979,7 +13990,7 @@ static void prvResetNextTaskUnblockTime( void )
/* If a task has timed out because it already holds the
* mutex it was trying to obtain then it cannot of inherited
* its own priority. */
(__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5440, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
(__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5451, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
/* Disinherit the priority, remembering the previous
* priority to facilitate determining the subject task's
@ -14110,7 +14121,7 @@ void vTaskYieldWithinAPI( void )
{
/* If pxCurrentTCB->uxCriticalNesting is zero then this function
* does not match a previous call to vTaskEnterCritical(). */
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5571, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5582, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
if( xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U )
{
@ -14160,11 +14171,11 @@ void vTaskYieldWithinAPI( void )
/*-----------------------------------------------------------*/
// # 5647 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5658 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 5753 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5764 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
// # 5880 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5891 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
TickType_t uxTaskResetEventItemValue( void )
@ -14206,7 +14217,7 @@ TickType_t uxTaskResetEventItemValue( void )
{
uint32_t ulReturn;
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5921, "uxIndexToWait < 1") : (void)0);
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5932, "uxIndexToWait < 1") : (void)0);
vTaskEnterCritical();
{
@ -14280,7 +14291,7 @@ TickType_t uxTaskResetEventItemValue( void )
{
BaseType_t xReturn;
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5995, "uxIndexToWait < 1") : (void)0);
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6006, "uxIndexToWait < 1") : (void)0);
vTaskEnterCritical();
{
@ -14368,8 +14379,8 @@ TickType_t uxTaskResetEventItemValue( void )
BaseType_t xReturn = ( ( ( BaseType_t ) 1 ) );
uint8_t ucOriginalNotifyState;
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6083, "uxIndexToNotify < 1") : (void)0);
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6084, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6094, "uxIndexToNotify < 1") : (void)0);
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6095, "xTaskToNotify") : (void)0);
pxTCB = xTaskToNotify;
vTaskEnterCritical();
@ -14422,7 +14433,7 @@ TickType_t uxTaskResetEventItemValue( void )
/* Should not get here if all enums are handled.
* Artificially force an assert by testing a value the
* compiler can't assume is const. */
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6137, "xTickCount == ( TickType_t ) 0") : (void)0);
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6148, "xTickCount == ( TickType_t ) 0") : (void)0);
break;
}
@ -14437,8 +14448,8 @@ TickType_t uxTaskResetEventItemValue( void )
; { if( ( ( pxTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxTCB )->uxPriority ] ), &( ( pxTCB )->xStateListItem ) ); ;
/* The task should not have been on an event list. */
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6152, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
// # 6171 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6163, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
// # 6182 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
prvYieldForTask( pxTCB, ( ( BaseType_t ) 0 ) );
}
@ -14471,8 +14482,8 @@ TickType_t uxTaskResetEventItemValue( void )
BaseType_t xReturn = ( ( ( BaseType_t ) 1 ) );
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6203, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6204, "uxIndexToNotify < 1") : (void)0);
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6214, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6215, "uxIndexToNotify < 1") : (void)0);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -14543,7 +14554,7 @@ TickType_t uxTaskResetEventItemValue( void )
/* Should not get here if all enums are handled.
* Artificially force an assert by testing a value the
* compiler can't assume is const. */
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6275, "xTickCount == ( TickType_t ) 0") : (void)0);
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6286, "xTickCount == ( TickType_t ) 0") : (void)0);
break;
}
@ -14554,7 +14565,7 @@ TickType_t uxTaskResetEventItemValue( void )
if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) )
{
/* The task should not have been on an event list. */
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6286, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6297, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) )
{
@ -14599,8 +14610,8 @@ TickType_t uxTaskResetEventItemValue( void )
uint8_t ucOriginalNotifyState;
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6331, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6332, "uxIndexToNotify < 1") : (void)0);
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6342, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6343, "uxIndexToNotify < 1") : (void)0);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -14638,7 +14649,7 @@ TickType_t uxTaskResetEventItemValue( void )
if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) )
{
/* The task should not have been on an event list. */
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6370, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6381, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) )
{
@ -14679,7 +14690,7 @@ TickType_t uxTaskResetEventItemValue( void )
TCB_t * pxTCB;
BaseType_t xReturn;
(__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6411, "uxIndexToClear < 1") : (void)0);
(__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6422, "uxIndexToClear < 1") : (void)0);
/* If null is passed in here then it is the calling task that is having
* its notification state cleared. */
@ -14732,7 +14743,7 @@ TickType_t uxTaskResetEventItemValue( void )
/*-----------------------------------------------------------*/
// # 6480 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 6491 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
@ -14808,7 +14819,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
}
}
}
// # 6592 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 6603 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
/* Code below here allows additional code to be inserted into this source file,

2
verification/verifast/proof/task_predicates.h
View file

@ -26,7 +26,7 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*&
// pcTaskName
// Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars_(tcb->pcTaskName, 16, _) &*&
tcb->uxCriticalNesting |-> _ &*&