diff --git a/tasks.c b/tasks.c index b5d84e206..f2a8c4055 100644 --- a/tasks.c +++ b/tasks.c @@ -1371,7 +1371,7 @@ static void prvYieldForTask( TCB_t * pxTCB, pxNewTCB->pxStack = pxStack; //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); - //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); + //@ close uninit_TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); } else { @@ -1431,7 +1431,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, TaskHandle_t * const pxCreatedTask, TCB_t * pxNewTCB, const MemoryRegion_t * const xRegions ) -/*@ requires TCB_p(pxNewTCB, ?stackSize) &*& +/*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*& stackSize == ulStackDepth * sizeof(StackType_t) &*& stackSize <= UINTPTR_MAX &*& ulStackDepth > 0 &*& @@ -1460,7 +1460,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, #endif /* portUSING_MPU_WRAPPERS == 1 */ - //@ open TCB_p(_,_); + //@ open uninit_TCB_p(_,_); /* Avoid dependency on memset() if it is not required. */ #if ( tskSET_NEW_STACKS_TO_KNOWN_VALUE == 1 ) @@ -1534,17 +1534,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, } #endif /* portSTACK_GROWTH */ - //@ close TCB_p(pxNewTCB, stackSize); + //@ close uninit_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) &*& + /*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*& chars(pcName, 16, _); @*/ { - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); pxNewTCB->pcTaskName[ x ] = pcName[ x ]; /* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than @@ -1556,29 +1556,29 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, * violation when we don't close the predicate? * This seems like a bug. */ - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); break; } else { mtCOVERAGE_TEST_MARKER(); } - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* Ensure the name string is terminated in the case that the string length * was greater or equal to configMAX_TASK_NAME_LEN. */ pxNewTCB->pcTaskName[ configMAX_TASK_NAME_LEN - 1 ] = '\0'; - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } else { - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* The task has not been given a name, so just ensure there is a NULL * terminator when it is read out. */ pxNewTCB->pcTaskName[ 0 ] = 0x00; - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } /* This is used as an array index so must ensure it's not too large. First @@ -1592,7 +1592,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, mtCOVERAGE_TEST_MARKER(); } - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); pxNewTCB->uxPriority = uxPriority; #if ( configUSE_MUTEXES == 1 ) { @@ -1600,12 +1600,12 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, pxNewTCB->uxMutexesHeld = 0; } #endif /* configUSE_MUTEXES */ - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* 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. */ @@ -1786,7 +1786,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, mtCOVERAGE_TEST_MARKER(); } - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } /*-----------------------------------------------------------*/ diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c index 16afe1f46..3b6a3efee 100644 --- a/verification/verifast/preprocessed_files/tasks--pp.c +++ b/verification/verifast/preprocessed_files/tasks--pp.c @@ -10032,9 +10032,10 @@ predicate xLIST_ITEM( /*@ + // This predicate represents the memory corresponding to an -// instance of type `TCB_t` aka `tskTaskControlBlock`. -predicate TCB_p(TCB_t * tcb, int stackSize) = +// uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`. +predicate uninit_TCB_p(TCB_t * tcb, int stackSize) = malloc_block_tskTaskControlBlock(tcb) &*& tcb->pxTopOfStack |-> _ &*& @@ -10070,8 +10071,6 @@ predicate TCB_p(TCB_t * tcb, int stackSize) = uchars_(tcb->ucNotifyState, 1, _) &*& tcb->ucDelayAborted |-> _; - - @*/ // # 52 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup/verifast_RP2040_axioms.h" 1 @@ -11023,7 +11022,7 @@ static void prvYieldForTask( TCB_t * pxTCB, pxNewTCB->pxStack = pxStack; //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); - //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); + //@ close uninit_TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); } else { @@ -11069,7 +11068,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, TaskHandle_t * const pxCreatedTask, TCB_t * pxNewTCB, const MemoryRegion_t * const xRegions ) -/*@ requires TCB_p(pxNewTCB, ?stackSize) &*& +/*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*& stackSize == ulStackDepth * sizeof(StackType_t) &*& stackSize <= UINTPTR_MAX &*& ulStackDepth > 0 &*& @@ -11082,7 +11081,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, StackType_t * pxTopOfStack; UBaseType_t x; // # 1463 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" - //@ open TCB_p(_,_); + //@ open uninit_TCB_p(_,_); /* Avoid dependency on memset() if it is not required. */ @@ -11131,17 +11130,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, // # 1523 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } // # 1537 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" - //@ close TCB_p(pxNewTCB, stackSize); + //@ close uninit_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) &*& + /*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*& chars(pcName, 16, _); @*/ { - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); pxNewTCB->pcTaskName[ x ] = pcName[ x ]; /* Don't copy all configMAX_TASK_NAME_LEN if the string is shorter than @@ -11153,29 +11152,29 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, * violation when we don't close the predicate? * This seems like a bug. */ - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); break; } else { ; } - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* Ensure the name string is terminated in the case that the string length * was greater or equal to configMAX_TASK_NAME_LEN. */ pxNewTCB->pcTaskName[ 16 - 1 ] = '\0'; - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } else { - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* The task has not been given a name, so just ensure there is a NULL * terminator when it is read out. */ pxNewTCB->pcTaskName[ 0 ] = 0x00; - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } /* This is used as an array index so must ensure it's not too large. First @@ -11189,7 +11188,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, ; } - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); pxNewTCB->uxPriority = uxPriority; { @@ -11197,12 +11196,12 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, pxNewTCB->uxMutexesHeld = 0; } - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); - //@ open TCB_p(_, _); + //@ open uninit_TCB_p(_, _); /* 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. */ @@ -11305,7 +11304,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, ; } - //@ close TCB_p(_, _); + //@ close uninit_TCB_p(_, _); } /*-----------------------------------------------------------*/ diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h index b222813bd..01b3c46f6 100644 --- a/verification/verifast/proof/task_predicates.h +++ b/verification/verifast/proof/task_predicates.h @@ -6,9 +6,10 @@ /*@ + // This predicate represents the memory corresponding to an -// instance of type `TCB_t` aka `tskTaskControlBlock`. -predicate TCB_p(TCB_t * tcb, int stackSize) = +// uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`. +predicate uninit_TCB_p(TCB_t * tcb, int stackSize) = malloc_block_tskTaskControlBlock(tcb) &*& tcb->pxTopOfStack |-> _ &*& @@ -44,8 +45,6 @@ predicate TCB_p(TCB_t * tcb, int stackSize) = uchars_(tcb->ucNotifyState, 1, _) &*& tcb->ucDelayAborted |-> _; - - @*/ #endif /* TASKS_GH */ \ No newline at end of file