diff options
Diffstat (limited to 'Source/Concurrency/Program.cs')
-rw-r--r-- | Source/Concurrency/Program.cs | 88 |
1 files changed, 44 insertions, 44 deletions
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index 8042476e..1be7cc07 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -1,44 +1,44 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-namespace Microsoft.Boogie
-{
- public class Concurrency
- {
- public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
- {
- 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))
- {
- originalDecls.Add(proc);
- continue;
- }
- Implementation impl = decl as Implementation;
- if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
- {
- originalDecls.Add(impl);
- }
- }
-
- List<Declaration> decls = new List<Declaration>();
- if (!CommandLineOptions.Clo.TrustAtomicityTypes)
- {
- MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
- }
- OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
- foreach (Declaration decl in decls)
- {
- decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
- }
- program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
- program.AddTopLevelDeclarations(decls);
- }
-
- }
-}
+using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Boogie +{ + public class Concurrency + { + 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 && civlTypeChecker.procToActionInfo.ContainsKey(proc)) + { + originalDecls.Add(proc); + continue; + } + Implementation impl = decl as Implementation; + if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) + { + originalDecls.Add(impl); + } + } + + List<Declaration> decls = new List<Declaration>(); + if (!CommandLineOptions.Clo.TrustAtomicityTypes) + { + MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls); + } + CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls); + foreach (Declaration decl in decls) + { + decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes); + } + program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x)); + program.AddTopLevelDeclarations(decls); + } + + } +} |