summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Concurrency/CivlTypeChecker.cs54
-rw-r--r--Test/civl/chris7.bpl14
-rw-r--r--Test/civl/chris7.bpl.expect2
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