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

Included global variables pxCurrentTCBs and pxYieldingPendings in interrupt invariant.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 13:53:22 -05:00
parent d63a8f83cd
commit 54523ecdce
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tasks.c
View file

@ -4136,7 +4136,8 @@ void vTaskSwitchContext( BaseType_t xCoreID )
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0); pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
@*/ @*/
//@ ensures true; //@ ensures true;
@ -4176,6 +4177,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
#endif /* VERIFAST */ #endif /* VERIFAST */
//@ open taskISRLockInv();
if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE ) if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
{ {
/* The scheduler is currently suspended - do not allow a context /* The scheduler is currently suspended - do not allow a context

5
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -28,7 +28,10 @@ predicate interruptState_p(uint32_t coreID, uint32_t state);
fixpoint bool interruptsDisabled_f(uint32_t); fixpoint bool interruptsDisabled_f(uint32_t);
predicate coreLocalInterruptInv_p() = predicate coreLocalInterruptInv_p() =
pointer(&pxCurrentTCBs[coreID_f], _); pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*&
pubTCB_p(currentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
predicate coreLocalLocked(uint32_t coreID); predicate coreLocalLocked(uint32_t coreID);
@*/ @*/