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

Adapted loop invariant to reflect potential change of state lists.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-04 10:46:05 -05:00
parent b594404b59
commit 61bffc4617
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tasks.c
View file

@ -988,7 +988,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
//@ open taskISRLockInv_p(); //@ open taskISRLockInv_p();
//@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates) ); //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates0) );
//@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ open readyLists_p(?gCellLists, ?gOwnerLists);
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
@ -1051,7 +1051,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
gSize > 0 &*& gSize > 0 &*&
exists_in_taskISRLockInv_p(gTasks, gStates) exists_in_taskISRLockInv_p(gTasks, ?gStates)
&*& &*&
// Read permissions for every task // Read permissions for every task
foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates))