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

Renamed TCB_p predicate into uninit_TCB_p.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-27 12:58:18 -04:00
parent e238d791ab
commit 551d1da628
3 changed files with 38 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

32
tasks.c
View file

@ -1371,7 +1371,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxNewTCB->pxStack = pxStack; pxNewTCB->pxStack = pxStack;
//@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
//@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); //@ 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 else
{ {
@ -1431,7 +1431,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
TaskHandle_t * const pxCreatedTask, TaskHandle_t * const pxCreatedTask,
TCB_t * pxNewTCB, TCB_t * pxNewTCB,
const MemoryRegion_t * const xRegions ) const MemoryRegion_t * const xRegions )
/*@ requires TCB_p(pxNewTCB, ?stackSize) &*& /*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*&
stackSize == ulStackDepth * sizeof(StackType_t) &*& stackSize == ulStackDepth * sizeof(StackType_t) &*&
stackSize <= UINTPTR_MAX &*& stackSize <= UINTPTR_MAX &*&
ulStackDepth > 0 &*& ulStackDepth > 0 &*&
@ -1460,7 +1460,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
#endif /* portUSING_MPU_WRAPPERS == 1 */ #endif /* portUSING_MPU_WRAPPERS == 1 */
//@ open TCB_p(_,_); //@ open uninit_TCB_p(_,_);
/* Avoid dependency on memset() if it is not required. */ /* Avoid dependency on memset() if it is not required. */
#if ( tskSET_NEW_STACKS_TO_KNOWN_VALUE == 1 ) #if ( tskSET_NEW_STACKS_TO_KNOWN_VALUE == 1 )
@ -1534,17 +1534,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
} }
#endif /* portSTACK_GROWTH */ #endif /* portSTACK_GROWTH */
//@ close TCB_p(pxNewTCB, stackSize); //@ 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 TCB_p(pxNewTCB, stackSize) &*& /*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*&
chars(pcName, 16, _); chars(pcName, 16, _);
@*/ @*/
{ {
//@ open TCB_p(_, _); //@ 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
@ -1556,29 +1556,29 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
* violation when we don't close the predicate? * violation when we don't close the predicate?
* This seems like a bug. * This seems like a bug.
*/ */
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
break; break;
} }
else else
{ {
mtCOVERAGE_TEST_MARKER(); 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 /* 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 TCB_p(_, _); //@ close uninit_TCB_p(_, _);
} }
else else
{ {
//@ open TCB_p(_, _); //@ open uninit_TCB_p(_, _);
/* The task has not been given a name, so just ensure there is a NULL /* The task has not been given a name, so just ensure there is a NULL
* terminator when it is read out. */ * terminator when it is read out. */
pxNewTCB->pcTaskName[ 0 ] = 0x00; 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 /* 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(); mtCOVERAGE_TEST_MARKER();
} }
//@ open TCB_p(_, _); //@ open uninit_TCB_p(_, _);
pxNewTCB->uxPriority = uxPriority; pxNewTCB->uxPriority = uxPriority;
#if ( configUSE_MUTEXES == 1 ) #if ( configUSE_MUTEXES == 1 )
{ {
@ -1600,12 +1600,12 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
pxNewTCB->uxMutexesHeld = 0; pxNewTCB->uxMutexesHeld = 0;
} }
#endif /* configUSE_MUTEXES */ #endif /* configUSE_MUTEXES */
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); 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 /* 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. */
@ -1786,7 +1786,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
mtCOVERAGE_TEST_MARKER(); mtCOVERAGE_TEST_MARKER();
} }
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
} }
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/

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

@ -10032,9 +10032,10 @@ predicate xLIST_ITEM(
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// instance of type `TCB_t` aka `tskTaskControlBlock`. // uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb, int stackSize) = predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxTopOfStack |-> _ &*& tcb->pxTopOfStack |-> _ &*&
@ -10070,8 +10071,6 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
uchars_(tcb->ucNotifyState, 1, _) &*& uchars_(tcb->ucNotifyState, 1, _) &*&
tcb->ucDelayAborted |-> _; tcb->ucDelayAborted |-> _;
@*/ @*/
// # 52 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 52 "/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
@ -11023,7 +11022,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxNewTCB->pxStack = pxStack; pxNewTCB->pxStack = pxStack;
//@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
//@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); //@ 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 else
{ {
@ -11069,7 +11068,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
TaskHandle_t * const pxCreatedTask, TaskHandle_t * const pxCreatedTask,
TCB_t * pxNewTCB, TCB_t * pxNewTCB,
const MemoryRegion_t * const xRegions ) const MemoryRegion_t * const xRegions )
/*@ requires TCB_p(pxNewTCB, ?stackSize) &*& /*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*&
stackSize == ulStackDepth * sizeof(StackType_t) &*& stackSize == ulStackDepth * sizeof(StackType_t) &*&
stackSize <= UINTPTR_MAX &*& stackSize <= UINTPTR_MAX &*&
ulStackDepth > 0 &*& ulStackDepth > 0 &*&
@ -11082,7 +11081,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
StackType_t * pxTopOfStack; StackType_t * pxTopOfStack;
UBaseType_t x; UBaseType_t x;
// # 1463 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" // # 1463 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ open TCB_p(_,_); //@ open uninit_TCB_p(_,_);
/* Avoid dependency on memset() if it is not required. */ /* 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" // # 1523 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
} }
// # 1537 "/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. */ /* 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 TCB_p(pxNewTCB, stackSize) &*& /*@ invariant uninit_TCB_p(pxNewTCB, stackSize) &*&
chars(pcName, 16, _); chars(pcName, 16, _);
@*/ @*/
{ {
//@ open TCB_p(_, _); //@ 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
@ -11153,29 +11152,29 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
* violation when we don't close the predicate? * violation when we don't close the predicate?
* This seems like a bug. * This seems like a bug.
*/ */
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
break; break;
} }
else 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 /* 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 TCB_p(_, _); //@ close uninit_TCB_p(_, _);
} }
else else
{ {
//@ open TCB_p(_, _); //@ open uninit_TCB_p(_, _);
/* The task has not been given a name, so just ensure there is a NULL /* The task has not been given a name, so just ensure there is a NULL
* terminator when it is read out. */ * terminator when it is read out. */
pxNewTCB->pcTaskName[ 0 ] = 0x00; 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 /* 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; pxNewTCB->uxPriority = uxPriority;
{ {
@ -11197,12 +11196,12 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
pxNewTCB->uxMutexesHeld = 0; pxNewTCB->uxMutexesHeld = 0;
} }
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); 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 /* 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. */
@ -11305,7 +11304,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
; ;
} }
//@ close TCB_p(_, _); //@ close uninit_TCB_p(_, _);
} }
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/

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

@ -6,9 +6,10 @@
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// instance of type `TCB_t` aka `tskTaskControlBlock`. // uninitialised instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb, int stackSize) = predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxTopOfStack |-> _ &*& tcb->pxTopOfStack |-> _ &*&
@ -44,8 +45,6 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
uchars_(tcb->ucNotifyState, 1, _) &*& uchars_(tcb->ucNotifyState, 1, _) &*&
tcb->ucDelayAborted |-> _; tcb->ucDelayAborted |-> _;
@*/ @*/
#endif /* TASKS_GH */ #endif /* TASKS_GH */