diff options
| -rw-r--r-- | Source/Concurrency/CivlTypeChecker.cs | 54 | ||||
| -rw-r--r-- | Test/civl/chris7.bpl | 14 | ||||
| -rw-r--r-- | Test/civl/chris7.bpl.expect | 2 |
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 |