diff options
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index d1c89965..5d0eab47 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -557,21 +557,22 @@ namespace Microsoft.Dafny foreach (Expression req in fn.Req) {
auto_reqs.AddRange(generateAutoReqs(req));
}
+ fn.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
+ addAutoReqToolTipInfo("pre", fn, auto_reqs);
// Then the body itself, if any
if (fn.Body != null) {
- auto_reqs.AddRange(generateAutoReqs(fn.Body));
- }
-
- fn.Req.InsertRange(0, auto_reqs);
- addAutoReqToolTipInfo(fn, auto_reqs);
+ auto_reqs = generateAutoReqs(fn.Body);
+ fn.Req.AddRange(auto_reqs);
+ addAutoReqToolTipInfo("post", fn, auto_reqs);
+ }
}
}
}
}
- public void addAutoReqToolTipInfo(Function f, List<Expression> reqs) {
- string prefix = "auto requires ";
+ public void addAutoReqToolTipInfo(string label, Function f, List<Expression> reqs) {
+ string prefix = "auto requires " + label + " ";
string tip = "";
foreach (var req in reqs) {
|