From aad91eb391f331b248969a6e6eac69908a798eca Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Fri, 17 Apr 2015 15:55:32 -0700
Subject: fixed the treatment of extern

---
 Source/Concurrency/MoverCheck.cs |  9 ++++-----
 Source/Concurrency/TypeCheck.cs  | 16 +++++++++-------
 2 files changed, 13 insertions(+), 12 deletions(-)

(limited to 'Source/Concurrency')

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 971e7271..ed069d5d 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -30,9 +30,9 @@ namespace Microsoft.Boogie
             if (moverTypeChecker.procToActionInfo.Count == 0)
                 return;
 
-            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));
+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
-            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));
+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
 
             Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
@@ -85,10 +85,9 @@ namespace Microsoft.Boogie
                     }
                 }
             }
-            foreach (ActionInfo actionInfo in moverTypeChecker.procToActionInfo.Values)
+            foreach (AtomicActionInfo atomicActionInfo in sortedByCreatedLayerNum)
             {
-                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
-                if (atomicActionInfo != null && atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)
+                if (atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)
                 {
                     moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);
                 }
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 845d2140..f37a7582 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -23,6 +23,7 @@ namespace Microsoft.Boogie
         public int createdAtLayerNum;
         public int availableUptoLayerNum;
         public bool hasImplementation;
+        public bool isExtern;
 
         public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)
         {
@@ -30,6 +31,7 @@ namespace Microsoft.Boogie
             this.createdAtLayerNum = createdAtLayerNum;
             this.availableUptoLayerNum = availableUptoLayerNum;
             this.hasImplementation = false;
+            this.isExtern = QKeyValue.FindBoolAttribute(proc.Attributes, "extern");
         }
 
         public virtual bool IsRightMover
@@ -369,7 +371,6 @@ namespace Microsoft.Boogie
             foreach (var proc in program.Procedures)
             {
                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
-                if (QKeyValue.FindBoolAttribute(proc.Attributes, "extern")) continue;
 
                 int createdAtLayerNum;  // must be initialized by the following code, otherwise it is an error
                 int availableUptoLayerNum = int.MaxValue;
@@ -444,16 +445,17 @@ namespace Microsoft.Boogie
             foreach (var proc in procToActionInfo.Keys)
             {
                 ActionInfo actionInfo = procToActionInfo[proc];
-                if (actionInfo.hasImplementation) continue;
-                if (leastUnimplementedLayerNum == int.MaxValue)
+                if (actionInfo.isExtern && actionInfo.hasImplementation)
                 {
-                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
+                    Error(proc, "Extern procedure cannot have an implementation");
+                    continue;
                 }
-                else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum)
+                if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
+                if (leastUnimplementedLayerNum == int.MaxValue)
                 {
-                    // do nothing
+                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
                 }
-                else
+                else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
                 {
                     Error(proc, "All unimplemented atomic actions must be created at the same layer");
                 }
-- 
cgit v1.2.3