diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 20 |
1 files changed, 14 insertions, 6 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; |