added a fix to check all layers: created layer of actions or layers in

requires, ensures, or asserts

3 files changed, 15 insertions, 20 deletions

diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index 8fc27be9..dfe50ef9 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
+            foreach (int layerNum in civlTypeChecker.AllLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 5215bc52..430c0d2c 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -486,20 +486,27 @@ namespace Microsoft.Boogie
             }
         }
 
-        private HashSet<int> allCreatedLayerNums;
-        public IEnumerable<int> AllCreatedLayerNums
+        private HashSet<int> allLayerNums;
+        public IEnumerable<int> AllLayerNums
         {
             get
             {
-                if (allCreatedLayerNums == null)
+                if (allLayerNums == null)
                 {
-                    allCreatedLayerNums = new HashSet<int>();
+                    allLayerNums = new HashSet<int>();
                     foreach (ActionInfo actionInfo in procToActionInfo.Values)
                     {
-                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
+                        allLayerNums.Add(actionInfo.createdAtLayerNum);
+                    }
+                    foreach (var layerNums in absyToLayerNums.Values)
+                    {
+                        foreach (var layer in layerNums)
+                        {
+                            allLayerNums.Add(layer);
+                        }
                     }
                 }
-                return allCreatedLayerNums;
+                return allLayerNums;
             }
         }
 
@@ -705,18 +712,6 @@ namespace Microsoft.Boogie
                     Error(impl.Proc, "Extern procedure cannot have an implementation");
                 }
             }
-            foreach (var g in this.globalVarToSharedVarInfo.Keys)
-            {
-                var info = globalVarToSharedVarInfo[g];
-                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
-                {
-                    Error(g, "Variable must be introduced with creation of some atomic action");
-                }
-                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
-                {
-                    Error(g, "Variable must be hidden with creation of some atomic action");
-                }
-            }
             if (errorCount > 0) return;
             this.VisitProgram(program);
             if (errorCount > 0) return;
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 027e7e83..ed59d3ad 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
                 int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
+                foreach (int layerNum in civlTypeChecker.AllLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
                     YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);