diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-13 16:36:59 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-13 16:36:59 -0800 |
| commit | c1341a323aa60f563a59355a0ede693c80dd2fc0 (patch) | |
| tree | 3059e0cbbeb2af08519dbabf403aced2dc41b3a9 /Source | |
| parent | 66bc974bd173d33e675bfbf399687c4882ec6014 (diff) | |
Small fix to the order in which AutoReq adds its requirements.
Diffstat (limited to 'Source')
| -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) {
|