summaryrefslogtreecommitdiff
path: root/Source/Concurrency/Program.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Concurrency/Program.cs')
-rw-r--r--Source/Concurrency/Program.cs88
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);
+ }
+
+ }
+}