changed the semantics of requires and ensures for inlined procedures

4 files changed, 42 insertions, 9 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 0f29c9a0..cae8bd92 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -533,6 +533,13 @@ namespace Microsoft.Boogie {
         return l.asBigNum.ToIntSafe;

       return defl;

     }

+

+    public override Absy Clone() {

+      List<object> newParams = new List<object>();

+      foreach (object o in Params)

+        newParams.Add(o);

+      return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());

+    }

   }

 

   public class Trigger : Absy {

@@ -546,7 +553,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(Pos || Tr.Length == 1);

     }

 

-

     public Trigger Next;

 

     public Trigger(IToken tok, bool pos, ExprSeq tr)

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 7519fb4c..645cdee5 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -587,7 +587,7 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
     (.

       // here we attach kv only to the Procedure, not its implementation

       impl = new Implementation(x, x.val, typeParams,

-                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);

+                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);

     .)

   )

   (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index adc7e2f0..c9f6445c 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -388,6 +388,27 @@ namespace Microsoft.Boogie {
       codeCopier.OldSubst = null;

     }

 

+    private Cmd InlinedRequires(Implementation impl, CallCmd callCmd, Requires req) {

+      Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

+      if (req.Free)

+        reqCopy.Condition = Expr.True;

+      else 

+        reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

+      AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);

+      a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

+      return a;

+    }

+

+    private Cmd InlinedEnsures(Implementation impl, CallCmd callCmd, Ensures ens) {

+      if (impl.FindExprAttribute("inline") != null && !ens.Free) {

+        Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());

+        ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

+        return new AssertEnsuresCmd(ensCopy);

+      }

+      else {

+        return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

+      }

+    }

 

     // result[0] is the entry block

     protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {

@@ -418,17 +439,20 @@ namespace Microsoft.Boogie {
         inCmds.Add(cmd);

       }

 

-      // inject non-free requires

+      // inject requires

       for (int i = 0; i < proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

+        inCmds.Add(InlinedRequires(impl, callCmd, req));

+        /*

         if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {

-          Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

+          Requires reqCopy = (Requires)cce.NonNull(req.Clone());

           reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

-          AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);

+          AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);

           Contract.Assert(a != null);

           a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

           inCmds.Add(a);

         }

+        */

       }

 

       VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);

@@ -483,16 +507,19 @@ namespace Microsoft.Boogie {
       // create out block

       CmdSeq outCmds = new CmdSeq();

 

-      // inject non-free ensures

+      // inject ensures

       for (int i = 0; i < proc.Ensures.Length; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

+        outCmds.Add(InlinedEnsures(impl, callCmd, ens));

+        /*

         if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {

-          Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());

+          Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());

           ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

-          AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);

+          AssertCmd a = new AssertEnsuresCmd(ensCopy);

           Contract.Assert(a != null);

           outCmds.Add(a);

         }

+        */

       }

 

       // assign out params

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 34f43896..5bfbbfc2 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -503,7 +503,7 @@ private class BvBounds : Expr {
 			}

 			ImplBody(out locals, out stmtList);

 			impl = new Implementation(x, x.val, typeParams,

-			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);

+			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);

 			

 		} else SynErr(91);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);