diff options
author | 2014-05-03 10:06:13 -0700 | |
---|---|---|
committer | 2014-05-03 10:06:13 -0700 | |
commit | 36e016acf963b7c19d59640b11b4a40f2072943e (patch) | |
tree | 31a45e868059d0ffe54fc3d212261245ff97886a /Source/Concurrency/Program.cs | |
parent | 121071b9f87d23eaeba176897b9655cd540fb694 (diff) |
checkpoint
Diffstat (limited to 'Source/Concurrency/Program.cs')
-rw-r--r-- | Source/Concurrency/Program.cs | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index a3a621ac..915eadda 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -9,22 +9,18 @@ namespace Microsoft.Boogie {
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"))
+ if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))
{
originalDecls.Add(proc);
continue;
}
Implementation impl = decl as Implementation;
- if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
{
originalDecls.Add(impl);
}
@@ -38,17 +34,7 @@ namespace Microsoft.Boogie }
foreach (Declaration decl in decls)
{
- Procedure proc = decl as Procedure;
- if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
- {
- proc.Modifies = new List<IdentifierExpr>();
- linearTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));
- }
- }
- foreach (Declaration decl in decls)
- {
decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
- decl.Attributes = OwickiGries.RemoveStableAttribute(decl.Attributes);
}
program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));
program.TopLevelDeclarations.AddRange(decls);
|