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

Applied closing lemmas.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-23 11:34:47 -05:00
parent be9de4d570
commit f44473b47c
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
tasks.c
View file

@ -1113,6 +1113,18 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
//@ assert( mem(gTaskItem_1, gCells) == true ); //@ assert( mem(gTaskItem_1, gCells) == true );
//@ close xLIST_ITEM(gTaskItem_0, _, _, _, gReadyList);
/*@
if( gTaskItem_0 == gListEnd ) {
DLS_end_next_close(gReadyList, gTaskItem_0);
} else {
DLS_nonEndItem_next_close(gReadyList, gTaskItem_0, gCells, gVals);
}
@*/
// unifying ghost branches
//@ assert( DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
//@ assume(false); //@ assume(false);
if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) )