From 21a496e6b7c93fff9fd14115b0ae26eb959d32e5 Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 27 Feb 2014 13:56:17 -0800 Subject: added some missing attributes to desugared assertions --- Source/Concurrency/OwickiGries.cs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'Source') 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(), new List()); } 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); } -- cgit v1.2.3