diff options
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/CivlRefinement.cs | 2 | ||||
| -rw-r--r-- | Source/Concurrency/CivlTypeChecker.cs | 20 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 2 |
3 files changed, 2 insertions, 22 deletions
diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs index 43d0f60c..8fc27be9 100644 --- a/Source/Concurrency/CivlRefinement.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index dba7ab4b..5215bc52 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -486,26 +486,6 @@ namespace Microsoft.Boogie } } - private HashSet<int> allImplementedLayerNums; - public IEnumerable<int> AllImplementedLayerNums - { - get - { - if (allImplementedLayerNums == null) - { - allImplementedLayerNums = new HashSet<int>(); - foreach (ActionInfo actionInfo in procToActionInfo.Values) - { - if (actionInfo.hasImplementation) - { - allImplementedLayerNums.Add(actionInfo.createdAtLayerNum); - } - } - } - return allImplementedLayerNums; - } - } - private HashSet<int> allCreatedLayerNums; public IEnumerable<int> AllCreatedLayerNums { diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index a69f066d..027e7e83 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie Graph<Block> implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); |