improved some of the annotations

2 files changed, 29 insertions, 29 deletions

diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl
index a6dfcb2a..11ba8afa 100644
--- a/Test/civl/Program4.bpl
+++ b/Test/civl/Program4.bpl
@@ -2,51 +2,51 @@
 // RUN: %diff "%s.expect" "%t"
 var {:layer 0,2} a:[int]int;
 var {:layer 0,1} count: int;
-var {:layer 1,1} {:linear "tid"} unallocated:[int]bool;
+var {:layer 1,1} {:linear "tid"} allocated:[int]bool;
 
 procedure {:yields} {:layer 2} main()
-requires {:layer 1} AllocInv(count, unallocated);
+requires {:layer 1} allocated == MapConstBool(false);
 {
     var {:layer 1} {:linear "tid"} tid:int;
     var i: int;
 
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     while (true)
-    invariant {:layer 1} AllocInv(count, unallocated);
+    invariant {:layer 1} AllocInv(count, allocated);
     { 
         call tid, i := Allocate(); 
 	async call P(tid, i); 
 	yield;
-        assert {:layer 1} AllocInv(count, unallocated);	
+        assert {:layer 1} AllocInv(count, allocated);	
     }
     yield;
 }
 
 procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int)
 requires {:layer 1} tid == i;
-requires {:layer 1} AllocInv(count, unallocated);
-ensures {:layer 1} AllocInv(count, unallocated);
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:layer 2} a[tid] == old(a)[tid] + 1; 
 { 
     var t:int;
 
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     assert {:layer 2} a[tid] == old(a)[tid];
     call t := Read(tid, i); 
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     assert {:layer 2} a[tid] == t; 
     call Write(tid, i, t + 1); 
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     assert {:layer 2} a[tid] == t + 1; 
 }
 
 procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int)
-requires {:layer 1} AllocInv(count, unallocated);
-ensures {:layer 1} AllocInv(count, unallocated);
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:layer 1} tid == i;
 ensures {:atomic}
 |{A:
@@ -54,48 +54,48 @@ ensures {:atomic}
 }|;
 {
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     call i := AllocateLow();
     call tid := MakeLinear(i);
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);    
+    assert {:layer 1} AllocInv(count, allocated);    
 }
 
 procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int)
 requires {:layer 1} tid == i;
-requires {:layer 1} AllocInv(count, unallocated);
-ensures {:layer 1} AllocInv(count, unallocated);
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:atomic}
 |{A:
   val := a[tid]; return true;
 }|;
 {
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     call val := ReadLow(i);
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
 }
 
 procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int)
 requires {:layer 1} tid == i;
-requires {:layer 1} AllocInv(count, unallocated);
-ensures {:layer 1} AllocInv(count, unallocated);
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:atomic}
 |{A:
   a[tid] := val; return true;
 }|;
 {
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
     call WriteLow(i, val);
     yield;
-    assert {:layer 1} AllocInv(count, unallocated);
+    assert {:layer 1} AllocInv(count, allocated);
 }
 
-function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool)
+function {:inline} AllocInv(count: int, allocated:[int]bool): (bool)
 {
-    (forall x: int :: count <= x ==> unallocated[x])
+    (forall x: int :: allocated[x] ==> x < count)
 }
 
 procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int);
@@ -121,9 +121,9 @@ ensures {:atomic}
 // We can prove that this primitive procedure preserves the permission invariant locally.
 // We only need to using its specification and the definitions of TidCollector and TidSetCollector.
 procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int);
-requires unallocated[i];
-modifies unallocated;
-ensures tid == i && unallocated == old(unallocated)[i := false];
+requires !allocated[i];
+modifies allocated;
+ensures tid == i && allocated == old(allocated)[i := true];
 
 function {:builtin "MapConst"} MapConstBool(bool): [int]bool;
 function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool;
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index bb0201a9..64e01c99 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -1,7 +1,7 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-const unique null: int;
+const null: int;
 type lmap;
 function {:linear "Node"} dom(lmap): [int]bool;
 function map(lmap): [int]int;
@@ -17,7 +17,7 @@ function Remove(x: lmap, i: int): (lmap);
 axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
 
 procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int);
-ensures {:right} |{ A: assume dom(Stack)[v] || Used[v]; return true; }|;
+ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|;
 
 procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int);
 ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C;