From 5cf8b4ed1c89c93e6f13ff82f3d79eb0a4628db1 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Mon, 21 Nov 2022 08:06:19 -0500
Subject: [PATCH] Added shared global variable `xSchedulerRunning` to task-isr
 lock invariant.

---
 verification/verifast/proof/verifast_lock_predicates.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 0a6117561..857604e79 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -87,7 +87,8 @@ predicate isrLockInv();
 fixpoint int taskISRLockID_f();
 
 predicate taskISRLockInv() = 
-    integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _)
+    integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
+    integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _)
     &*&
     // top ready priority must be in range
         integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&