diff options
| author |  qadeer <unknown> | 2013-12-20 21:10:25 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-20 21:10:25 -0800 |
| commit | 123afb33cd5137cc685bbe4faf2aab387ee0de72 (patch) | |
| tree | 3c13d6f7cb12dccab16ca80b811e910572b8fd78 /Source/Concurrency/Program.cs | |
| parent | 9030a5a43425e5bf3c44a15cbfa0031ba4435c9e (diff) | |
more refactoring of the concurrency stuff
Diffstat (limited to 'Source/Concurrency/Program.cs')
| -rw-r--r-- | Source/Concurrency/Program.cs | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs new file mode 100644 index 00000000..592667c8 --- /dev/null +++ b/Source/Concurrency/Program.cs @@ -0,0 +1,43 @@ +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)
+ {
+ // The order in which originalDecls are computed and then *.AddCheckers are called is
+ // apparently important. The MyDuplicator code currently does not duplicate Attributes.
+ // Consequently, all the yield attributes are eliminated by the AddCheckers code.
+
+ List<Declaration> originalDecls = new List<Declaration>();
+ Program program = linearTypeChecker.program;
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+ {
+ originalDecls.Add(proc);
+ continue;
+ }
+ Implementation impl = decl as Implementation;
+ if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ {
+ originalDecls.Add(impl);
+ }
+ }
+
+ List<Declaration> decls = new List<Declaration>();
+ OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+ MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+ RefinementCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+
+ program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));
+ program.TopLevelDeclarations.AddRange(decls);
+ }
+
+ }
+}
|