InlineAssume attribute for ensures clauses; if present, the ensures condition is assumed while inlining.

2 files changed, 5 insertions, 2 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 49273f94..31b38e8a 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2412,7 +2412,7 @@ namespace Microsoft.Boogie.Houdini {
                     QKeyValue.FindStringAttribute(ens.Attributes, "post") == null)

                 .Iter(ens => nensures.Add(ens));

                 foreach (Ensures en in nensures)

-                    en.Attributes = removeAttr("HoudiniAssume", en.Attributes);

+                    en.Attributes = removeAttr("InlineAssume", en.Attributes);

 

                 proc.Ensures = nensures;

             }

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index d8adf7d3..6bb2d4db 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -296,7 +296,10 @@ namespace Microsoft.Boogie.Houdini {
   public class InlineEnsuresVisitor : ReadOnlyVisitor {

       public override Ensures VisitEnsures(Ensures ensures)

       {

-          ensures.Attributes = new QKeyValue(Token.NoToken, "HoudiniAssume", new List<object>(), ensures.Attributes);

+          if (!ensures.Free)

+          {

+              ensures.Attributes = new QKeyValue(Token.NoToken, "InlineAssume", new List<object>(), ensures.Attributes);

+          }

           return base.VisitEnsures(ensures);

       }

   }