bug fix

3 files changed, 52 insertions, 18 deletions

diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index b0ea678c..71feb927 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -675,6 +675,36 @@ namespace Microsoft.Boogie
                 }
             }
             if (errorCount > 0) return;
+            
+            foreach (var impl in program.Implementations)
+            {
+                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+                ActionInfo actionInfo = procToActionInfo[impl.Proc];
+                procToActionInfo[impl.Proc].hasImplementation = true;
+                if (actionInfo.isExtern)
+                {
+                    Error(impl.Proc, "Extern procedure cannot have an implementation");
+                }
+            }
+            if (errorCount > 0) return;
+
+            foreach (Procedure proc in procToActionInfo.Keys)
+            {
+                for (int i = 0; i < proc.InParams.Count; i++)
+                {
+                    Variable v = proc.InParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                }
+                for (int i = 0; i < proc.OutParams.Count; i++)
+                {
+                    Variable v = proc.OutParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                }
+            }
             foreach (Implementation node in program.Implementations)
             {
                 if (!procToActionInfo.ContainsKey(node.Proc)) continue;
@@ -687,32 +717,20 @@ namespace Microsoft.Boogie
                 for (int i = 0; i < node.Proc.InParams.Count; i++)
                 {
                     Variable v = node.Proc.InParams[i];
-                    var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum);
-                    if (layer == int.MinValue) continue;
-                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
                     localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer);
                 }
                 for (int i = 0; i < node.Proc.OutParams.Count; i++)
                 {
                     Variable v = node.Proc.OutParams[i];
-                    var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum);
-                    if (layer == int.MinValue) continue;
-                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
                     localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer);
                 }
             }
-            if (errorCount > 0) return;
-            foreach (var impl in program.Implementations)
-            {
-                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
-                ActionInfo actionInfo = procToActionInfo[impl.Proc];
-                procToActionInfo[impl.Proc].hasImplementation = true;
-                if (actionInfo.isExtern)
-                {
-                    Error(impl.Proc, "Extern procedure cannot have an implementation");
-                }
-            }
-            if (errorCount > 0) return;
+            if (errorCount > 0) return; 
+            
             this.VisitProgram(program);
             if (errorCount > 0) return;
             YieldTypeChecker.PerformYieldSafeCheck(this);
diff --git a/Test/civl/chris7.bpl b/Test/civl/chris7.bpl
new file mode 100644
index 00000000..a8fd25d3
--- /dev/null
+++ b/Test/civl/chris7.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:layer 1}{:extern} P() returns(i:int);
+
+procedure{:yields}{:layer 1,1}{:extern} Y({:layer 1}x:int);
+
+procedure{:yields}{:layer 1,2} A({:layer 1}y:int)
+  ensures {:atomic} |{ A: return true; }|;
+{
+  var{:layer 1} tmp:int;
+  call Y(y);
+  call tmp := P();
+  call Y(tmp);
+}
diff --git a/Test/civl/chris7.bpl.expect b/Test/civl/chris7.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris7.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors