added variable hiding

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

1 files changed, 0 insertions, 19 deletions

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)) {