diff options
Diffstat (limited to 'Source/Concurrency/Program.cs')
| -rw-r--r-- | Source/Concurrency/Program.cs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index b56e1cf3..1be7cc07 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -7,20 +7,20 @@ namespace Microsoft.Boogie { public class Concurrency { - public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) + public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker) { List<Declaration> originalDecls = new List<Declaration>(); Program program = linearTypeChecker.program; foreach (var decl in program.TopLevelDeclarations) { Procedure proc = decl as Procedure; - if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc)) + if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc)) { originalDecls.Add(proc); continue; } Implementation impl = decl as Implementation; - if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) + if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) { originalDecls.Add(impl); } @@ -29,12 +29,12 @@ namespace Microsoft.Boogie List<Declaration> decls = new List<Declaration>(); if (!CommandLineOptions.Clo.TrustAtomicityTypes) { - MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls); } - OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls); foreach (Declaration decl in decls) { - decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes); + decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes); } program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x)); program.AddTopLevelDeclarations(decls); |