added some missing attributes to desugared assertions

1 files changed, 5 insertions, 5 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 6886a104..786df939 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -455,11 +455,11 @@ namespace Microsoft.Boogie
                     Substitution subst = Substituter.SubstitutionFromHashtable(map);

                     foreach (Requires req in callCmd.Proc.Requires)

                     {

-                        requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null));

+                        requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));

                     }

                     foreach (Ensures ens in callCmd.Proc.Ensures)

                     {

-                        ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null));

+                        ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));

                     }

                     count++;

                 }

@@ -467,7 +467,7 @@ namespace Microsoft.Boogie
                 proc.AddAttribute("yields");

                 asyncAndParallelCallDesugarings[procName] = proc;

             }

-            CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs);

+            CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);

             dummyCallCmd.Proc = proc;

             newCmds.Add(dummyCallCmd);

         }

@@ -550,7 +550,7 @@ namespace Microsoft.Boogie
                 }

                 else

                 {

-                    AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr);

+                    AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr, ensures.Attributes);

                     assertCmd.ErrorData = "Backwards non-interference check failed";

                     newCmds.Add(assertCmd);

                 }

@@ -854,7 +854,7 @@ namespace Microsoft.Boogie
                                 asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());

                             }

                             var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

-                            CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

+                            CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);

                             dummyCallCmd.Proc = dummyAsyncTargetProc;

                             newCmds.Add(dummyCallCmd);

                         }