fixed the treatment of extern

1 files changed, 9 insertions, 7 deletions

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

                 }