added variable hiding

added annotation on an atomic action about the phases in which it exists

4 files changed, 7 insertions, 21 deletions

diff --git a/Test/og/Answer b/Test/og/Answer
index f50f6d98..4b880cac 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -114,7 +114,7 @@ Boogie program verifier finished with 6 verified, 0 errors
 

 -------------------- multiset.bpl --------------------

 

-Boogie program verifier finished with 102 verified, 0 errors

+Boogie program verifier finished with 104 verified, 0 errors

 

 -------------------- civl-paper.bpl --------------------

 

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 4ebaadbe..0449a166 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -100,7 +100,7 @@ ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock
 }

 

 procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

-ensures {:atomic 0} |{ 

+ensures {:atomic 0,1} |{ 

 A: goto B, C; 

 B: assume b == prev; b := next; status := true; lock := tid; return true; 

 C: status := false; return true; 

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 161171bf..5bb056f3 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -41,7 +41,7 @@ ensures {:left 0} |{ A:
 

 

 procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

-ensures {:both 0} |{ A: 

+ensures {:both 0,1} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

                      assert tidIn != nil && tidIn != done;

@@ -52,7 +52,7 @@ ensures {:both 0} |{ A:
 

 

 procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:both 0} |{ A: 

+ensures {:both 0,1} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

                      assert 0 <= j && j < max;

@@ -78,20 +78,6 @@ ensures {:left 0} |{ A:
                      return true;

                     }|;

 

-

-

-

-procedure {:yields} getValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, valid_j:bool);

-ensures {:both 0} |{ A: 

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil  && tidIn != done;

-                     tidOut := tidIn;

-	             valid_j := valid[j];

-                     return true;

-                    }|;

-

-

 procedure {:yields} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

 ensures {:both 0} |{ A: 

                      assert 0 <= j && j < max;

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 3404f8e0..953230e7 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -95,7 +95,7 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil
 procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T, t);

-ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

+ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

     tid := tid';

@@ -125,10 +125,10 @@ procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"}
 ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

 procedure {:yields} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

-ensures {:atomic 0} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

+ensures {:atomic 0,1} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

 

 procedure {:yields} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

+ensures {:atomic 0,2} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

 

 procedure {:yields} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

 ensures {:atomic 0} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;