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

Renamed predicate encapsulating access permissions to core local variables to coreLocalInterruptInv_p.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 11:31:12 -05:00
parent 327423ef67
commit d63a8f83cd
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -27,7 +27,7 @@ predicate interruptState_p(uint32_t coreID, uint32_t state);
fixpoint bool interruptsDisabled_f(uint32_t);
predicate coreLocalGlobalVars_p() =
predicate coreLocalInterruptInv_p() =
pointer(&pxCurrentTCBs[coreID_f], _);
predicate coreLocalLocked(uint32_t coreID);

4
verification/verifast/proof/verifast_port_contracts.h
View file

@ -35,7 +35,7 @@ uint32_t VF__portDISABLE_INTERRUPTS();
/*@ ensures result == state &*&
interruptState_p(coreID, ?newState) &*&
interruptsDisabled_f(newState) == true &*&
coreLocalGlobalVars_p();
coreLocalInterruptInv_p();
@*/
#undef portRESTORE_INTERRUPTS
@ -43,7 +43,7 @@ uint32_t VF__portDISABLE_INTERRUPTS();
void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
/*@ requires interruptState_p(?coreID, ?tmpState) &*&
interruptsDisabled_f(tmpState) == true
? coreLocalGlobalVars_p()
? coreLocalInterruptInv_p()
: true;
@*/
/*@ ensures interruptState_p(coreID, ulState);