From 5927744da636063556118f469cc8f9354b1cabe6 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <qadeer@microsoft.com>
Date: Fri, 25 Sep 2015 12:05:19 -0700
Subject: added introduced and ghost local variables

---
 Test/civl/lock-introduced.bpl | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'Test/civl/lock-introduced.bpl')

diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index fa0a3977..5403e5d4 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -67,6 +67,9 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
     yield;
     L: 
         call status := CAS(false, true);
+        if (status) {
+	    call SetLock(tid);
+	}
 	yield;
         goto A, B;
 
@@ -85,9 +88,16 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
 {
     yield;
     call SET(false);
+    call SetLock(nil);
     yield;
 }
 
+procedure {:layer 1} {:inline 1} SetLock(v: X)
+modifies lock;
+{
+    lock := v;
+}
+
 procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
 ensures {:atomic} |{ 
 A: goto B, C; 
-- 
cgit v1.2.3