diff options
| -rw-r--r-- | Source/Core/Inline.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 5 |
3 files changed, 6 insertions, 3 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 00aa5631..fe61a765 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -516,7 +516,7 @@ namespace Microsoft.Boogie { }
private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {
- if (QKeyValue.FindBoolAttribute(ens.Attributes, "HoudiniAssume")) {
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) {
return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
} else if (ens.Free) {
return new AssumeCmd(ens.tok, Expr.True);
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);
}
}
|