From e194828cb1051612dda9a6c51696fed7abc69cd3 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 16 Apr 2014 14:23:07 -0700
Subject: added variable hiding added annotation on an atomic action about the
 phases in which it exists

---
 Source/Core/Absy.cs | 19 -------------------
 1 file changed, 19 deletions(-)

(limited to 'Source/Core')

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)) {
-- 
cgit v1.2.3