diff options
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 20 | ||||
| -rw-r--r-- | Test/civl/chris3.bpl.expect | 5 |
2 files changed, 16 insertions, 9 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 793012e6..542d3515 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -388,11 +388,6 @@ namespace Microsoft.Boogie Error(proc, "Incorrect number of layers"); continue; } - if (availableUptoLayerNum <= createdAtLayerNum) - { - Error(proc, "Creation layer number must be less than the available upto layer number"); - continue; - } foreach (Ensures e in proc.Ensures) { MoverType moverType = GetMoverType(e); @@ -408,6 +403,11 @@ namespace Microsoft.Boogie Error(proc, "A procedure can have at most one atomic action"); continue; } + if (availableUptoLayerNum <= createdAtLayerNum) + { + Error(proc, "Creation layer number must be less than the available upto layer number"); + continue; + } minLayerNum = int.MaxValue; maxLayerNum = -1; @@ -432,7 +432,15 @@ namespace Microsoft.Boogie if (errorCount > 0) continue; if (!procToActionInfo.ContainsKey(proc)) { - procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); + if (availableUptoLayerNum < createdAtLayerNum) + { + Error(proc, "Creation layer number must be no more than the available upto layer number"); + continue; + } + else + { + procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); + } } } if (errorCount > 0) return; diff --git a/Test/civl/chris3.bpl.expect b/Test/civl/chris3.bpl.expect index c8b2ab00..b415d3b9 100644 --- a/Test/civl/chris3.bpl.expect +++ b/Test/civl/chris3.bpl.expect @@ -1,3 +1,2 @@ -chris3.bpl(3,33): Error: Creation layer number must be less than the available upto layer number -chris3.bpl(14,33): Error: Creation layer number must be less than the available upto layer number -2 type checking errors detected in chris3.bpl +chris3.bpl(17,2): Error: The callee is not available in the caller procedure +1 type checking errors detected in chris3.bpl |