diff options
author | qadeer <unknown> | 2014-01-13 14:51:33 -0800 |
---|---|---|
committer | qadeer <unknown> | 2014-01-13 14:51:33 -0800 |
commit | 451b7bfe5296ed2bd3568363294438b14df08fed (patch) | |
tree | 657401424e0d89f0b27f28de438927ed82eaf5c1 /Source/Concurrency | |
parent | c0ac4aa6760b48ac9dd05da8b6530d763277e096 (diff) |
eliminated use of assertionPhaseNums
Diffstat (limited to 'Source/Concurrency')
-rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index ebbb4abe..d7c6b5c2 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -94,24 +94,6 @@ namespace Microsoft.Boogie #endif
}
- private static HashSet<int> ComputePhaseIntervals(MoverTypeChecker moverTypeChecker)
- {
- HashSet<int> phases = new HashSet<int>();
- foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
- {
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
- int phaseNum = moverTypeChecker.FindPhaseNumber(proc);
- if (phaseNum != int.MaxValue) phases.Add(moverTypeChecker.FindPhaseNumber(proc));
-
- }
- foreach (int phs in moverTypeChecker.assertionPhaseNums)
- {
- phases.Add(phs);
- }
- return phases;
- }
-
private static Tuple<Automaton<BvSet>, bool> IsYieldReachabilitySafe(Automaton<BvSet> implReachabilityCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)
{
List<BvSet> witnessSet;
@@ -187,7 +169,7 @@ namespace Microsoft.Boogie Program yieldTypeCheckedProgram = moverTypeChecker.program;
YieldTypeChecker regExprToAuto = new YieldTypeChecker();
- HashSet<int> phases = ComputePhaseIntervals(moverTypeChecker);
+ HashSet<int> phases = moverTypeChecker.allPhaseNums;
foreach (int yTypeCheckCurrentPhaseNum in phases) // take current phase check num from each interval
{
foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)
|