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

Adapted first half of prvInitialiseNewTask to new stack predicate.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-01 16:06:53 -04:00
parent af090b252d
commit 800a7204bc
4 changed files with 127 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

19
tasks.c
View file

@ -1535,7 +1535,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
//@ bitand_def((int) pxTopOfStack, gzAlignedTop, gMask, gzMask); //@ bitand_def((int) pxTopOfStack, gzAlignedTop, gMask, gzMask);
configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) ); configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) );
/*@ /*@
if( pxTopOfStack < gOldTop ) if( pxTopOfStack < gOldTop )
{ {
@ -1544,7 +1544,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
@*/ @*/
//@ assert( chars(gcStack, ?gFreeBytes, _) ); //@ assert( chars(gcStack, ?gFreeBytes, _) );
//@ close stack_p_2(pxNewTCB->pxStack, ulStackDepth, pxTopOfStack, gFreeBytes, 0, gUnalignedBytes); //@ close stack_p_2(pxNewTCB->pxStack, ulStackDepth, pxTopOfStack, gFreeBytes, 0, gUnalignedBytes);
//@ assert(false);
#if ( configRECORD_STACK_HIGH_ADDRESS == 1 ) #if ( configRECORD_STACK_HIGH_ADDRESS == 1 )
@ -1568,17 +1567,14 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
} }
#endif /* portSTACK_GROWTH */ #endif /* portSTACK_GROWTH */
//@ close uninit_TCB_p(pxNewTCB, stackSize);
/* Store the task name in the TCB. */ /* Store the task name in the TCB. */
if( pcName != NULL ) if( pcName != NULL )
{ {
for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) configMAX_TASK_NAME_LEN; x++ ) for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) configMAX_TASK_NAME_LEN; x++ )
/*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*& /*@ invariant chars_(pxNewTCB->pcTaskName, 16, _) &*&
chars(pcName, 16, _); chars(pcName, 16, _);
@*/ @*/
{ {
//@ open uninit_TCB_p(_, _);
pxNewTCB->pcTaskName[ x ] = pcName[ x ]; pxNewTCB->pcTaskName[ x ] = pcName[ x ];
/* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than /* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than
@ -1586,25 +1582,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
* string is not accessible (extremely unlikely). */ * string is not accessible (extremely unlikely). */
if( pcName[ x ] == ( char ) 0x00 ) if( pcName[ x ] == ( char ) 0x00 )
{ {
/* TODO: Why does VeriFast not report a loop invariant
* violation when we don't close the predicate?
* This seems like a bug.
*/
//@ close uninit_TCB_p(_, _);
break; break;
} }
else else
{ {
mtCOVERAGE_TEST_MARKER(); mtCOVERAGE_TEST_MARKER();
} }
//@ close uninit_TCB_p(_, _);
} }
//@ open uninit_TCB_p(_, _);
/* Ensure the name string is terminated in the case that the string length /* Ensure the name string is terminated in the case that the string length
* was greater or equal to configMAX_TASK_NAME_LEN. */ * was greater or equal to configMAX_TASK_NAME_LEN. */
pxNewTCB->pcTaskName[ configMAX_TASK_NAME_LEN - 1 ] = '\0'; pxNewTCB->pcTaskName[ configMAX_TASK_NAME_LEN - 1 ] = '\0';
//@ close uninit_TCB_p(_, _);
} }
else else
{ {
@ -1626,7 +1614,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
mtCOVERAGE_TEST_MARKER(); mtCOVERAGE_TEST_MARKER();
} }
//@ open uninit_TCB_p(_, _);
pxNewTCB->uxPriority = uxPriority; pxNewTCB->uxPriority = uxPriority;
#if ( configUSE_MUTEXES == 1 ) #if ( configUSE_MUTEXES == 1 )
{ {
@ -1634,12 +1621,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
pxNewTCB->uxMutexesHeld = 0; pxNewTCB->uxMutexesHeld = 0;
} }
#endif /* configUSE_MUTEXES */ #endif /* configUSE_MUTEXES */
//@ close uninit_TCB_p(_, _);
vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); vListInitialiseItem( &( pxNewTCB->xEventListItem ) );
//@ open uninit_TCB_p(_, _);
/* Set the pxNewTCB as a link back from the ListItem_t. This is so we can get /* Set the pxNewTCB as a link back from the ListItem_t. This is so we can get
* back to the containing TCB from a generic item in a list. */ * back to the containing TCB from a generic item in a list. */

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

@ -9962,6 +9962,7 @@ predicate stack_p_2(StackType_t * pxStack,
uint32_t ulFreeBytes, uint32_t ulFreeBytes,
uint32_t ulUsedCells, uint32_t ulUsedCells,
uint32_t ulUnalignedBytes) = uint32_t ulUnalignedBytes) =
malloc_block_chars((char*) pxStack, ulStackDepth * sizeof(StackType_t)) &*&
// Free stack cells. The size of this memory block is not necessarily a // Free stack cells. The size of this memory block is not necessarily a
// multiple of sizeof(StackType_t), due to bitvector arithmetic. // multiple of sizeof(StackType_t), due to bitvector arithmetic.
// At least, we cannot prove it. // At least, we cannot prove it.
@ -10063,7 +10064,6 @@ predicate xLIST_ITEM(
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`. // uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate uninit_TCB_p(TCB_t * tcb, int stackSize) = predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
@ -10104,6 +10104,47 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
tcb->ucDelayAborted |-> _; tcb->ucDelayAborted |-> _;
@*/ @*/
/*@
// This predicate represents the memory corresponding to an
// initialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*&
xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*&
xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*&
tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*&
// Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars_(tcb->pcTaskName, 16, _) &*&
tcb->uxCriticalNesting |-> _ &*&
tcb->uxTCBNumber |-> _ &*&
tcb->uxTaskNumber |-> _ &*&
tcb->uxBasePriority |-> _ &*&
tcb->uxMutexesHeld |-> _ &*&
// void * pvThreadLocalStoragePointers[ 5 ];
pointers_(tcb->pvThreadLocalStoragePointers, 5, _) &*&
// We assume that the macro `configTASK_NOTIFICATION_ARRAY_ENTRIES`
// evaluates to 1.
integers__(tcb->ulNotifiedValue, 4, false, 1, _) &*&
uchars_(tcb->ucNotifyState, 1, _) &*&
tcb->ucDelayAborted |-> _;
@*/
// # 60 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 60 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2
// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup/verifast_RP2040_axioms.h" 1 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup/verifast_RP2040_axioms.h" 1
@ -11251,21 +11292,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
@*/ @*/
//@ assert( chars(gcStack, ?gFreeBytes, _) ); //@ assert( chars(gcStack, ?gFreeBytes, _) );
//@ close stack_p_2(pxNewTCB->pxStack, ulStackDepth, pxTopOfStack, gFreeBytes, 0, gUnalignedBytes); //@ close stack_p_2(pxNewTCB->pxStack, ulStackDepth, pxTopOfStack, gFreeBytes, 0, gUnalignedBytes);
//@ assert(false); // # 1556 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1557 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
// # 1571 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1570 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ close uninit_TCB_p(pxNewTCB, stackSize);
/* Store the task name in the TCB. */ /* Store the task name in the TCB. */
if( pcName != 0 ) if( pcName != 0 )
{ {
for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) 16; x++ ) for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) 16; x++ )
/*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*& /*@ invariant chars_(pxNewTCB->pcTaskName, 16, _) &*&
chars(pcName, 16, _); chars(pcName, 16, _);
@*/ @*/
{ {
//@ open uninit_TCB_p(_, _);
pxNewTCB->pcTaskName[ x ] = pcName[ x ]; pxNewTCB->pcTaskName[ x ] = pcName[ x ];
/* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than /* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than
@ -11273,25 +11310,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
* string is not accessible (extremely unlikely). */ * string is not accessible (extremely unlikely). */
if( pcName[ x ] == ( char ) 0x00 ) if( pcName[ x ] == ( char ) 0x00 )
{ {
/* TODO: Why does VeriFast not report a loop invariant
* violation when we don't close the predicate?
* This seems like a bug.
*/
//@ close uninit_TCB_p(_, _);
break; break;
} }
else else
{ {
; ;
} }
//@ close uninit_TCB_p(_, _);
} }
//@ open uninit_TCB_p(_, _);
/* Ensure the name string is terminated in the case that the string length /* Ensure the name string is terminated in the case that the string length
* was greater or equal to configMAX_TASK_NAME_LEN. */ * was greater or equal to configMAX_TASK_NAME_LEN. */
pxNewTCB->pcTaskName[ 16 - 1 ] = '\0'; pxNewTCB->pcTaskName[ 16 - 1 ] = '\0';
//@ close uninit_TCB_p(_, _);
} }
else else
{ {
@ -11313,7 +11342,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
; ;
} }
//@ open uninit_TCB_p(_, _);
pxNewTCB->uxPriority = uxPriority; pxNewTCB->uxPriority = uxPriority;
{ {
@ -11321,12 +11349,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
pxNewTCB->uxMutexesHeld = 0; pxNewTCB->uxMutexesHeld = 0;
} }
//@ close uninit_TCB_p(_, _);
vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); vListInitialiseItem( &( pxNewTCB->xEventListItem ) );
//@ open uninit_TCB_p(_, _);
/* Set the pxNewTCB as a link back from the ListItem_t. This is so we can get /* Set the pxNewTCB as a link back from the ListItem_t. This is so we can get
* back to the containing TCB from a generic item in a list. */ * back to the containing TCB from a generic item in a list. */
@ -11344,7 +11370,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{ {
pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U; pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U;
} }
// # 1679 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1664 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
/* Avoid compiler warning about unreferenced parameter. */ /* Avoid compiler warning about unreferenced parameter. */
( void ) xRegions; ( void ) xRegions;
@ -11371,7 +11397,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
//@ uchars__to_chars_(pxNewTCB->ucNotifyState); //@ uchars__to_chars_(pxNewTCB->ucNotifyState);
memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) ); memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) );
} }
// # 1717 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1702 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
/* Reason for rewrite: Assignment not type safe. */ /* Reason for rewrite: Assignment not type safe. */
@ -11380,17 +11406,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
} }
// # 1740 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1725 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Initialize the TCB stack to look as if the task was already running, /* 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 * 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 * to the start of the task function. Once the stack has been initialised
* the top of stack variable is updated. */ * the top of stack variable is updated. */
// # 1768 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1753 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
/* If the port has capability to detect stack overflow, /* If the port has capability to detect stack overflow,
* pass the stack end address to the stack initialization * pass the stack end address to the stack initialization
* function as well. */ * function as well. */
// # 1785 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1770 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters ); pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters );
} }
@ -12099,13 +12125,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 2527 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 2512 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 2550 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 2535 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 2568 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 2553 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 2596 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 2581 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
@ -12472,7 +12498,7 @@ static BaseType_t prvCreateIdleTasks( void )
{ {
; ;
} }
// # 3009 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 2994 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
if( xCoreID == 0 ) if( xCoreID == 0 )
{ {
@ -12484,7 +12510,7 @@ static BaseType_t prvCreateIdleTasks( void )
( ( UBaseType_t ) 0x00 ), /* In effect ( tskIDLE_PRIORITY | portPRIVILEGE_BIT ), but tskIDLE_PRIORITY is zero. */ ( ( 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. */ &xIdleTaskHandle[ xCoreID ] ); /*lint !e961 MISRA exception, justified as it is not a redundant explicit cast to all supported compilers. */
} }
// # 3032 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3017 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
} }
@ -12521,7 +12547,7 @@ void vTaskStartScheduler( void )
* so interrupts will automatically get re-enabled when the first task * so interrupts will automatically get re-enabled when the first task
* starts to run. */ * starts to run. */
assert_fct(false); assert_fct(false);
// # 3082 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3067 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL; xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL;
xSchedulerRunning = ( ( char ) 1 ); xSchedulerRunning = ( ( char ) 1 );
xTickCount = ( TickType_t ) 0; xTickCount = ( TickType_t ) 0;
@ -12618,7 +12644,7 @@ void vTaskSuspendAll( void )
} }
} }
/*----------------------------------------------------------*/ /*----------------------------------------------------------*/
// # 3240 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3225 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/ /*----------------------------------------------------------*/
BaseType_t xTaskResumeAll( void ) BaseType_t xTaskResumeAll( void )
@ -12988,7 +13014,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
* each task in the Suspended state. */ * each task in the Suspended state. */
uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended ); uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended );
} }
// # 3623 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3608 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
if( pulTotalRunTime != 0 ) if( pulTotalRunTime != 0 )
{ {
@ -13027,7 +13053,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
* This is to ensure vTaskStepTick() is available when user defined low power mode * 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 * implementations require configUSE_TICKLESS_IDLE to be set to a value other than
* 1. */ * 1. */
// # 3674 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3659 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/ /*----------------------------------------------------------*/
BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp ) BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
@ -13337,13 +13363,13 @@ BaseType_t xTaskIncrementTick( void )
return xSwitchRequired; return xSwitchRequired;
} }
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4012 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 3997 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4036 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4021 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4061 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4046 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4094 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4079 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
void vTaskSwitchContext( BaseType_t xCoreID ) void vTaskSwitchContext( BaseType_t xCoreID )
@ -13373,7 +13399,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
{ {
xYieldPendings[ xCoreID ] = ( ( char ) 0 ); xYieldPendings[ xCoreID ] = ( ( char ) 0 );
; ;
// # 4152 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4137 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Check for stack overflow, if configured. */ /* 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 ); } }; { 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 ); } };
@ -13390,7 +13416,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
; ;
/* After the new task is switched in, update the global errno. */ /* After the new task is switched in, update the global errno. */
// # 4186 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4171 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
} }
vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 )); vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 ));
@ -13503,7 +13529,7 @@ BaseType_t xTaskRemoveFromEventList( const List_t * const pxEventList )
{ {
( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) ); ( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) );
; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ; ; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ;
// # 4312 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4297 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
else else
{ {
@ -13543,7 +13569,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
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. */ 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. */
assert(pxUnblockedTCB); assert(pxUnblockedTCB);
( void ) uxListRemove( pxEventListItem ); ( void ) uxListRemove( pxEventListItem );
// # 4366 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4351 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Remove the task from the delayed list and add it to the ready list. The /* 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 * scheduler is suspended so interrupts will not be accessing the ready
* lists. */ * lists. */
@ -13708,7 +13734,7 @@ void vTaskMissedYield( void )
* *
* @todo additional conditional compiles to remove this function. * @todo additional conditional compiles to remove this function.
*/ */
// # 4590 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4575 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* /*
* ----------------------------------------------------------- * -----------------------------------------------------------
* The Idle task. * The Idle task.
@ -13738,7 +13764,7 @@ static void prvIdleTask( void * pvParameters )
/* See if any tasks have deleted themselves - if so then the idle task /* See if any tasks have deleted themselves - if so then the idle task
* is responsible for freeing the deleted task's TCB and stack. */ * is responsible for freeing the deleted task's TCB and stack. */
prvCheckTasksWaitingTermination(); prvCheckTasksWaitingTermination();
// # 4631 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4616 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
/* When using preemption tasks of equal priority will be /* When using preemption tasks of equal priority will be
* timesliced. If a task that is sharing the idle priority is ready * timesliced. If a task that is sharing the idle priority is ready
@ -13759,16 +13785,16 @@ static void prvIdleTask( void * pvParameters )
; ;
} }
} }
// # 4667 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4652 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* This conditional compilation should use inequality to 0, not equality /* This conditional compilation should use inequality to 0, not equality
* to 1. This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when * to 1. This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when
* user defined low power mode implementations require * user defined low power mode implementations require
* configUSE_TICKLESS_IDLE to be set to a value other than 1. */ * configUSE_TICKLESS_IDLE to be set to a value other than 1. */
// # 4732 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4717 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
} }
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4782 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4767 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
@ -13813,7 +13839,7 @@ static void prvIdleTask( void * pvParameters )
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 4842 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4827 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
static void prvInitialiseTaskLists( void ) static void prvInitialiseTaskLists( void )
@ -13915,7 +13941,7 @@ static void prvCheckTasksWaitingTermination( void )
{ {
pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority; pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority;
} }
// # 4954 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 4939 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
pxTaskStatus->ulRunTimeCounter = 0; pxTaskStatus->ulRunTimeCounter = 0;
} }
@ -14046,7 +14072,7 @@ static void prvCheckTasksWaitingTermination( void )
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 5123 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 5108 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
@ -14103,7 +14129,7 @@ static void prvCheckTasksWaitingTermination( void )
free( (void*) pxTCB->pxStack); free( (void*) pxTCB->pxStack);
free( (void*) pxTCB); free( (void*) pxTCB);
} }
// # 5206 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 5191 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
@ -14603,11 +14629,11 @@ void vTaskYieldWithinAPI( void )
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 5731 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 5716 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 5837 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 5822 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/ /*----------------------------------------------------------*/
// # 5964 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 5949 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
TickType_t uxTaskResetEventItemValue( void ) TickType_t uxTaskResetEventItemValue( void )
@ -14881,7 +14907,7 @@ TickType_t uxTaskResetEventItemValue( void )
/* The task should not have been on an event list. */ /* The task should not have been on an event list. */
assert(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0); assert(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0);
// # 6255 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 6240 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{ {
prvYieldForTask( pxTCB, ( ( char ) 0 ) ); prvYieldForTask( pxTCB, ( ( char ) 0 ) );
} }
@ -15175,7 +15201,7 @@ TickType_t uxTaskResetEventItemValue( void )
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
// # 6564 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 6549 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
@ -15251,7 +15277,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
} }
} }
} }
// # 6676 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 6661 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
/* Code below here allows additional code to be inserted into this source file, /* Code below here allows additional code to be inserted into this source file,

1
verification/verifast/proof/stack_predicates.h
View file

@ -10,6 +10,7 @@ predicate stack_p_2(StackType_t * pxStack,
uint32_t ulFreeBytes, uint32_t ulFreeBytes,
uint32_t ulUsedCells, uint32_t ulUsedCells,
uint32_t ulUnalignedBytes) = uint32_t ulUnalignedBytes) =
malloc_block_chars((char*) pxStack, ulStackDepth * sizeof(StackType_t)) &*&
// Free stack cells. The size of this memory block is not necessarily a // Free stack cells. The size of this memory block is not necessarily a
// multiple of sizeof(StackType_t), due to bitvector arithmetic. // multiple of sizeof(StackType_t), due to bitvector arithmetic.
// At least, we cannot prove it. // At least, we cannot prove it.

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

@ -6,7 +6,6 @@
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`. // uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate uninit_TCB_p(TCB_t * tcb, int stackSize) = predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
@ -48,4 +47,45 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
tcb->ucDelayAborted |-> _; tcb->ucDelayAborted |-> _;
@*/ @*/
/*@
// This predicate represents the memory corresponding to an
// initialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*&
xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*&
xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*&
tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*&
// Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
chars_(tcb->pcTaskName, 16, _) &*&
tcb->uxCriticalNesting |-> _ &*&
tcb->uxTCBNumber |-> _ &*&
tcb->uxTaskNumber |-> _ &*&
tcb->uxBasePriority |-> _ &*&
tcb->uxMutexesHeld |-> _ &*&
// void * pvThreadLocalStoragePointers[ 5 ];
pointers_(tcb->pvThreadLocalStoragePointers, 5, _) &*&
// We assume that the macro `configTASK_NOTIFICATION_ARRAY_ENTRIES`
// evaluates to 1.
integers__(tcb->ulNotifiedValue, 4, false, 1, _) &*&
uchars_(tcb->ucNotifyState, 1, _) &*&
tcb->ucDelayAborted |-> _;
@*/
#endif /* TASKS_GH */ #endif /* TASKS_GH */