diff options
| author |  qadeer <unknown> | 2014-09-18 09:33:33 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-09-18 09:33:33 -0700 |
| commit | d1d367b1e9fb1cde673332030ef68b230c22dd06 (patch) | |
| tree | ad14b94d32a7fac1c18b872f79294abda3a05384 | |
| parent | 0c35477ac7e7fb5b73b3c64e301e09cd876c0703 (diff) | |
InlineAssume attribute for ensures clauses; if present, the ensures condition is assumed while inlining.
| -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);
}
}
|