fixed the treatment of extern

2 files changed, 13 insertions, 12 deletions

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");

                 }