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

Proved that pxTaskItem points to valid list item before inner search loop.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-21 14:02:23 -05:00
parent de3657239f
commit 35aef80072
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
tasks.c
View file

@ -1017,11 +1017,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious; ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious;
ListItem_t * pxTaskItem = pxLastTaskItem; ListItem_t * pxTaskItem = pxLastTaskItem;
/*@ /*@
if( gIndex == gListEnd ) { if( gIndex == gListEnd ) {
close xLIST_ITEM(gIndex, _, _, gEndPrev, &pxReadyTasksLists[uxCurrentPriority]); close xLIST_ITEM(gIndex, _, _, gEndPrev, &pxReadyTasksLists[uxCurrentPriority]);
close DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]); close DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]);
// Loop invariant for inner search loop below requires us
// to prove that `pxTaskItem` points to a valid list item.
dls_last_mem(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells);
assert( mem(pxTaskItem, gCells) == true );
} else { } else {
int gCellIndex = index_of(gIndex, gCells); int gCellIndex = index_of(gIndex, gCells);
assert( DLS( gListEnd, gEndPrev, gIndex, ?gIndexPrev, take(gCellIndex, gCells), take(gCellIndex, gVals), &pxReadyTasksLists[uxCurrentPriority]) ); assert( DLS( gListEnd, gEndPrev, gIndex, ?gIndexPrev, take(gCellIndex, gCells), take(gCellIndex, gVals), &pxReadyTasksLists[uxCurrentPriority]) );
@ -1033,7 +1037,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
gIndex, gIndexPrev, gListEnd, gEndPrev, drop(gCellIndex, gCells), drop(gCellIndex, gVals) ); gIndex, gIndexPrev, gListEnd, gEndPrev, drop(gCellIndex, gCells), drop(gCellIndex, gVals) );
} }
@*/ @*/
// Unified ghost breanches // Unified ghost branches
//@ assert( DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]) ); //@ assert( DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]) );
//@ open DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]); //@ open DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, &pxReadyTasksLists[uxCurrentPriority]);