added variable hiding

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

8 files changed, 152 insertions, 121 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index adfcc5c9..db2bfb23 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -9,23 +9,39 @@ namespace Microsoft.Boogie
 {

     public class MoverCheck

     {

-        public static MoverType GetMoverType(Ensures e, out int phaseNum)

+        public static MoverType GetMoverType(Ensures e, out int phaseNum, out int availableUptoPhaseNum)

         {

-            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "atomic", int.MaxValue);

-            if (phaseNum != int.MaxValue)

+            if (FindAtomicAction(e.Attributes, "atomic", out phaseNum, out availableUptoPhaseNum))

                 return MoverType.Atomic;

-            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "right", int.MaxValue);

-            if (phaseNum != int.MaxValue)

+            if (FindAtomicAction(e.Attributes, "right", out phaseNum, out availableUptoPhaseNum))

                 return MoverType.Right;

-            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "left", int.MaxValue);

-            if (phaseNum != int.MaxValue)

+            if (FindAtomicAction(e.Attributes, "left", out phaseNum, out availableUptoPhaseNum))

                 return MoverType.Left;

-            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "both", int.MaxValue);

-            if (phaseNum != int.MaxValue)

+            if (FindAtomicAction(e.Attributes, "both", out phaseNum, out availableUptoPhaseNum))

                 return MoverType.Both;

             return MoverType.Top;

         }

 

+        private static bool FindAtomicAction(QKeyValue kv, string name, out int phaseNum, out int availableUptoPhaseNum)

+        {

+            phaseNum = int.MaxValue;

+            availableUptoPhaseNum = int.MaxValue;

+            for (; kv != null; kv = kv.Next)

+            {

+                if (kv.Key != name) continue;

+                if (!(kv.Params.Count == 1 || kv.Params.Count == 2)) continue;

+                LiteralExpr l0 = kv.Params[0] as LiteralExpr;

+                if (l0 == null || !l0.isBigNum) continue;

+                phaseNum = l0.asBigNum.ToIntSafe;

+                if (kv.Params.Count == 1) return true;

+                LiteralExpr l1 = kv.Params[1] as LiteralExpr;

+                if (l1 == null || !l1.isBigNum) continue;

+                availableUptoPhaseNum = l1.asBigNum.ToIntSafe;

+                return true;

+            }

+            return false;

+        }

+

         LinearTypeChecker linearTypeChecker;

         MoverTypeChecker moverTypeChecker;

         List<Declaration> decls;

@@ -50,13 +66,16 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<ActionInfo>> pools = new Dictionary<int, HashSet<ActionInfo>>();

             foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)

             {

-                foreach (int phaseNum in action.callerPhaseNums)

+                foreach (int phaseNum in moverTypeChecker.allPhaseNums)

                 {

-                    if (!pools.ContainsKey(phaseNum))

+                    if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum)

                     {

-                        pools[phaseNum] = new HashSet<ActionInfo>();

+                        if (!pools.ContainsKey(phaseNum))

+                        {

+                            pools[phaseNum] = new HashSet<ActionInfo>();

+                        }

+                        pools[phaseNum].Add(action);

                     }

-                    pools[phaseNum].Add(action);

                 }

             }

 

@@ -457,6 +476,8 @@ namespace Microsoft.Boogie
             {

                 domainNameToScope[domainName] = new HashSet<Variable>();

             }

+            /*

+            // Commenting this out to avoid the danger of making an assumption about a hidden variable

             foreach (Variable v in program.GlobalVariables())

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

@@ -464,6 +485,7 @@ namespace Microsoft.Boogie
                 if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

+             */ 

             if (first != null)

             {

                 foreach (Variable v in first.thatInParams)

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index b5d41b21..9de83635 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Boogie
     {

         MoverTypeChecker moverTypeChecker;

         public int phaseNum;

-        int enclosingProcPhaseNum;

+        Procedure enclosingProc;

         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

         public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */

         public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */

@@ -22,7 +22,7 @@ namespace Microsoft.Boogie
         {

             this.moverTypeChecker = moverTypeChecker;

             this.phaseNum = phaseNum;

-            this.enclosingProcPhaseNum = int.MaxValue;

+            this.enclosingProc = null;

             this.procMap = new Dictionary<Procedure, Procedure>();

             this.absyMap = new Dictionary<Absy, Absy>();

             this.blockMap = new Dictionary<Block, Block>();

@@ -30,6 +30,11 @@ namespace Microsoft.Boogie
 

         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)

         {

+            int enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(enclosingProc);

+            if (enclosingProcPhaseNum == int.MaxValue)

+            {

+                enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();

+            }

             Procedure originalProc = originalCallCmd.Proc;

             if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

             {

@@ -137,6 +142,7 @@ namespace Microsoft.Boogie
 

         public override Procedure VisitProcedure(Procedure node)

         {

+            enclosingProc = node;

             if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))

                 return node;

             if (!procMap.ContainsKey(node))

@@ -164,11 +170,7 @@ namespace Microsoft.Boogie
         private Variable dummyLocalVar;

         public override Implementation VisitImplementation(Implementation node)

         {

-            enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc);

-            if (enclosingProcPhaseNum == int.MaxValue)

-            {

-                enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();

-            }

+            enclosingProc = node.Proc;

             dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));

             Implementation impl = base.VisitImplementation(node);

             impl.LocVars.Add(dummyLocalVar);

@@ -206,7 +208,8 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);

             if (node.Free)

                 return ensures;

-            if (ensures.IsAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))

+            bool isAtomicSpecification = moverTypeChecker.procToActionInfo.ContainsKey(enclosingProc) && moverTypeChecker.procToActionInfo[enclosingProc].ensures == ensures;

+            if (isAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))

             {

                 ensures.Condition = Expr.True;

                 ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 27a4e6a5..a8266e79 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -20,9 +20,10 @@ namespace Microsoft.Boogie
     public class ActionInfo

     {

         public Procedure proc;

+        public Ensures ensures;

         public MoverType moverType;

         public int phaseNum;

-        public HashSet<int> callerPhaseNums;

+        public int availableUptoPhaseNum;

         public List<AssertCmd> thisGate;

         public CodeExpr thisAction;

         public List<Variable> thisInParams;

@@ -55,12 +56,14 @@ namespace Microsoft.Boogie
             get { return moverType == MoverType.Left || moverType == MoverType.Both; }

         }

 

-        public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)

+        public ActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)

         {

+            CodeExpr codeExpr = ensures.Condition as CodeExpr;

             this.proc = proc;

+            this.ensures = ensures;

             this.moverType = moverType;

             this.phaseNum = phaseNum;

-            this.callerPhaseNums = new HashSet<int>();

+            this.availableUptoPhaseNum = availableUptoPhaseNum;

             this.thisGate = new List<AssertCmd>();

             this.thisAction = codeExpr;

             this.thisInParams = new List<Variable>();

@@ -186,19 +189,17 @@ namespace Microsoft.Boogie
             else

                 return int.MaxValue;

         }

-        public HashSet<Variable> QedGlobalVariables()

-        {

-            return qedGlobalVariables;

-        }

 

         CheckingContext checkingContext;

         public int errorCount;

-        HashSet<Variable> qedGlobalVariables;

-        int enclosingProcPhaseNum;

+        Dictionary<Variable, int> qedGlobalVariables;

+        Procedure enclosingProc;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

         public HashSet<int> allPhaseNums;

         bool inAtomicSpecification;

+        bool inSpecification;

+        int minPhaseNum;

 

         public void TypeCheck()

         {

@@ -208,8 +209,8 @@ namespace Microsoft.Boogie
                 if (proc == null) continue;

                 foreach (Ensures e in proc.Ensures)

                 {

-                    int phaseNum;

-                    MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum);

+                    int phaseNum, availableUptoPhaseNum;

+                    MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum, out availableUptoPhaseNum);

                     if (moverType == MoverType.Top) continue;

                     CodeExpr codeExpr = e.Condition as CodeExpr;

                     if (codeExpr == null)

@@ -222,16 +223,16 @@ namespace Microsoft.Boogie
                         Error(proc, "A procedure can have at most one atomic action");

                         continue;

                     }

-                    ActionInfo actionInfo = new ActionInfo(proc, codeExpr, moverType, phaseNum);

-                    /*

-                     * Removing this restriction based on the new failure preservation check

-                    if (actionInfo.IsLeftMover && !actionInfo.isNonBlocking)

+                    if (phaseNum >= availableUptoPhaseNum)

                     {

-                        Error(e, "A left mover must be non blocking");

+                        Error(proc, "Available at phase number should be less than available up to phase number");

                         continue;

                     }

-                     */ 

-                    procToActionInfo[proc] = actionInfo;

+                    if (phaseNum != int.MaxValue)

+                    {

+                        allPhaseNums.Add(phaseNum);

+                    }

+                    procToActionInfo[proc] = new ActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);

                 }

             }

             this.VisitProgram(program);

@@ -242,12 +243,19 @@ namespace Microsoft.Boogie
 

         public MoverTypeChecker(Program program)

         {

-            this.qedGlobalVariables = new HashSet<Variable>();

+            this.qedGlobalVariables = new Dictionary<Variable, int>();

             foreach (var g in program.GlobalVariables())

             {

                 if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))

                 {

-                    this.qedGlobalVariables.Add(g);

+                    this.qedGlobalVariables.Add(g, int.MaxValue);

+                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

+                }

+                else

+                {

+                    int phaseNum = QKeyValue.FindIntAttribute(g.Attributes, "qed", int.MaxValue);

+                    if (phaseNum == int.MaxValue) continue;

+                    this.qedGlobalVariables.Add(g, phaseNum);

                     g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

                 }

             }

@@ -256,36 +264,43 @@ namespace Microsoft.Boogie
             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

             this.program = program;

-            this.enclosingProcPhaseNum = int.MaxValue;

+            this.enclosingProc = null;

             this.inAtomicSpecification = false;

+            this.inSpecification = false;

+            this.minPhaseNum = int.MaxValue;

         }

         public override Implementation VisitImplementation(Implementation node)

         {

-            enclosingProcPhaseNum = FindPhaseNumber(node.Proc);

+            this.enclosingProc = node.Proc;

             return base.VisitImplementation(node);

         }

         public override Procedure VisitProcedure(Procedure node)

         {

-            enclosingProcPhaseNum = FindPhaseNumber(node);

-            if (enclosingProcPhaseNum != int.MaxValue)

-            {

-                allPhaseNums.Add(enclosingProcPhaseNum);

-            }

+            this.enclosingProc = node;

             return base.VisitProcedure(node);

         }

         public override Cmd VisitCallCmd(CallCmd node)

         {

             if (!node.IsAsync)

             {

+                int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);

                 int calleePhaseNum = FindPhaseNumber(node.Proc);

-                if (enclosingProcPhaseNum > calleePhaseNum)

+                if (enclosingProcPhaseNum == int.MaxValue)

                 {

-                    procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum);

+

                 }

-                else if (enclosingProcPhaseNum < calleePhaseNum || enclosingProcPhaseNum != int.MaxValue)

+                else if (calleePhaseNum == int.MaxValue)

+                {

+                    Error(node, "An atomic procedure cannot call a non-atomic procedure");

+                }

+                else if (enclosingProcPhaseNum <= calleePhaseNum)

                 {

                     Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

                 }

+                else if (procToActionInfo[node.Proc].availableUptoPhaseNum < enclosingProcPhaseNum)

+                {

+                    Error(node, "The callee is not available in the phase of the caller procedure");

+                }

             }

             return base.VisitCallCmd(node);

         }

@@ -298,7 +313,7 @@ namespace Microsoft.Boogie
                 if (calleePhaseNum > maxCalleePhaseNum)

                     maxCalleePhaseNum = calleePhaseNum;

             }

-

+            int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);

             if (enclosingProcPhaseNum > maxCalleePhaseNum)

             {

                 bool isLeftMover = true;

@@ -308,24 +323,32 @@ namespace Microsoft.Boogie
                     ActionInfo actionInfo = procToActionInfo[iter.Proc];

                     isLeftMover = isLeftMover && actionInfo.IsLeftMover;

                     isRightMover = isRightMover && actionInfo.IsRightMover;

-                    actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum);

                 }

                 if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)

                 {

                     Error(node, "The procedures in the parallel call must be all right mover or all left mover");

                 }

+                return base.VisitParCallCmd(node);

+            }

+            else

+            {

+                return node;

             }

-            return node;

         }

         public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

             if (node.Decl is GlobalVariable)

             {

-                if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))

+                if (qedGlobalVariables.ContainsKey(node.Decl) && qedGlobalVariables[node.Decl] < minPhaseNum)

+                {

+                    minPhaseNum = qedGlobalVariables[node.Decl];

+                }

+

+                if (inAtomicSpecification && !qedGlobalVariables.ContainsKey(node.Decl))

                 {

                     Error(node, "Cannot access non-qed global variable in atomic action");

                 }

-                else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))

+                else if (!inSpecification && qedGlobalVariables.ContainsKey(node.Decl))

                 {

                     Error(node, "Cannot access qed global variable in ordinary code");

                 }

@@ -334,47 +357,63 @@ namespace Microsoft.Boogie
         }

         public override Ensures VisitEnsures(Ensures ensures)

         {

-            if (ensures.IsAtomicSpecification)

+            minPhaseNum = int.MaxValue;

+            inAtomicSpecification = procToActionInfo.ContainsKey(enclosingProc) && procToActionInfo[enclosingProc].ensures == ensures;

+            inSpecification = true;

+            Ensures ret = base.VisitEnsures(ensures);

+            inSpecification = false;

+            if (inAtomicSpecification)

             {

-                inAtomicSpecification = true;

-                Ensures ret = base.VisitEnsures(ensures);

+                if (procToActionInfo[enclosingProc].availableUptoPhaseNum > minPhaseNum)

+                {

+                    Error(ensures, "A variable being accessed is hidden before this action becomes unavailable");

+                }

                 inAtomicSpecification = false;

-                return ret;

             }

-            foreach (int phaseNum in OwickiGries.FindPhaseNums(ensures.Attributes))

+            else

             {

-                allPhaseNums.Add(phaseNum);

-                if (phaseNum > enclosingProcPhaseNum)

-                {

-                    Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");

-                }

+                CheckAndAddPhases(ensures, ensures.Attributes);

             }

-            return ensures;

+            return ret;

         }

         public override Requires VisitRequires(Requires requires)

         {

-            foreach (int phaseNum in OwickiGries.FindPhaseNums(requires.Attributes))

-            {

-                allPhaseNums.Add(phaseNum);

-                if (phaseNum > enclosingProcPhaseNum)

-                {

-                    Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");

-                }

-            }

-            return requires;

+            minPhaseNum = int.MaxValue;

+            inSpecification = true;

+            Requires ret = base.VisitRequires(requires);

+            inSpecification = false;

+            CheckAndAddPhases(requires, requires.Attributes);

+            return ret;

         }

         public override Cmd VisitAssertCmd(AssertCmd node)

         {

-            foreach (int phaseNum in OwickiGries.FindPhaseNums(node.Attributes))

+            minPhaseNum = int.MaxValue;

+            inSpecification = true;

+            Cmd ret = base.VisitAssertCmd(node);

+            inSpecification = false;

+            CheckAndAddPhases(node, node.Attributes);

+            return ret;

+        }

+

+        private void CheckAndAddPhases(Absy node, QKeyValue attributes)

+        {

+            foreach (int phaseNum in OwickiGries.FindPhaseNums(attributes))

             {

-                allPhaseNums.Add(phaseNum);

-                if (phaseNum > enclosingProcPhaseNum)

+                if (phaseNum > FindPhaseNumber(enclosingProc))

                 {

-                    Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");

+                    Error(node, "The phase cannot be greater than the phase of enclosing procedure");

+                }

+                else if (phaseNum > minPhaseNum)

+                {

+                    Error(node, "A variable being accessed is hidden before this specification becomes unavailable");

+                }

+                else

+                {

+                    allPhaseNums.Add(phaseNum);

                 }

             }

-            return node;

         }

+

         public void Error(Absy node, string message)

         {

             checkingContext.Error(node, message);

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 60f76232..0bf55b17 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2364,26 +2364,7 @@ namespace Microsoft.Boogie {
       this.Condition.Resolve(rc);

     }

     

-    public bool IsAtomicSpecification

-    {

-        get

-        {

-            return

-                QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||

-                QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||

-                QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||

-                QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;

-        }

-    }

-

     public override void Typecheck(TypecheckingContext tc) {

-      //Contract.Requires(tc != null);

-        

-      if (IsAtomicSpecification && !tc.Yields)

-      {

-          tc.Error(this, "atomic specification allowed only in a yielding procedure");

-          return;

-      }

       this.Condition.Typecheck(tc);

       Contract.Assert(this.Condition.Type != null);  // follows from postcondition of Expr.Typecheck

       if (!this.Condition.Type.Unify(Type.Bool)) {

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; }|;