added an example

3 files changed, 137 insertions, 3 deletions

diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl
new file mode 100644
index 00000000..ad5bf271
--- /dev/null
+++ b/Test/civl/funky.bpl
@@ -0,0 +1,133 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+var {:layer 0, 3} A: X;
+var {:layer 0, 3} B: X;
+var {:layer 0, 3} counter: int;
+
+procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+
+procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X);
+ensures tid != nil;
+
+procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|;
+{
+    yield;
+    call DecrB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+{
+    yield;
+    call AssertA(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+{
+    yield;
+    call AssertB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+{
+    yield;
+    call LockA(tid);
+    call IncrA(tid);
+    call DecrA(tid);
+    call UnlockA(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|;
+{
+    yield;
+    call LockB(tid);
+    call AbsDecrB(tid);
+    call IncrB(tid);
+    call UnlockB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+    yield;
+    assert {:layer 3} counter == 0;
+    call TB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 3} main({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+    var {:linear "tid"} cid: X;
+    
+    yield;
+    assert {:layer 3} counter == 0;
+    while (*)
+    invariant {:layer 3} counter == 0;
+    {
+        if (*) {
+	    call cid := AllocTid();
+	    async call TA(cid);
+	}
+	if (*) {
+	    call cid := AllocTid();
+	    async call AbsTB(cid);
+	}
+    	yield;
+    	assert {:layer 3} counter == 0;
+	call LockA(tid);
+	call AbsAssertA(tid);
+	call LockB(tid);
+	call AbsAssertB(tid);
+	call UnlockB(tid);
+	call UnlockA(tid);
+	yield;
+    	assert {:layer 3} counter == 0;	
+    }
+    yield;
+}
\ No newline at end of file
diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect
new file mode 100644
index 00000000..0a114594
--- /dev/null
+++ b/Test/civl/funky.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 75 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 9fc55646..df19aae4 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
 axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 
 type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
 const nil: X;
 var {:layer 0,2} t: int;
 var {:layer 0,2} s: int;
@@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil;
 }
 
 procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == mapconstbool(true);
+requires {:layer 2} xls' == MapConstBool(true);
 {
     var {:linear "tid"} tid: X;
     var {:linear "tid"} xls: [X]bool;
@@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t);
 }
 
 procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
-ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
 
 procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
 ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;