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

Added missing task-ISR lock invariant to post condition of acquision lemma.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-11 15:07:01 -05:00
parent 29e14be203
commit d746a27233
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -126,7 +126,8 @@ requires locked(?heldLocks) &*&
heldLocks == cons(?i, cons(?t, nil)) &*& heldLocks == cons(?i, cons(?t, nil)) &*&
i == pair(?f_isr, isrLockID_f()) &*& i == pair(?f_isr, isrLockID_f()) &*&
t == pair(?f_task, taskLockID_f()); t == pair(?f_task, taskLockID_f());
ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ); ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*&
taskISRLockInv();
@*/ @*/