diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-27 14:50:37 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-27 14:50:37 -0700 |
| commit | 7114dca3c279789cd1d544bb5b80b0f699df8f59 (patch) | |
| tree | 1c8bbbb01c0d3a19cf53f1930d0479a50118a56d /Source/Dafny/Rewriter.cs | |
| parent | a00a390c15af08d71aa836540a5f1af1a65b82c2 (diff) | |
Don't process opaque functions more than once when generating auto-reqs
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 66 |
1 files changed, 33 insertions, 33 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 66cad286..67e425c3 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -689,43 +689,43 @@ namespace Microsoft.Dafny parentFunction = fn; // Remember where the recursion started
containsMatch = false; // Assume no match statements are involved
- List<Expression> auto_reqs = new List<Expression>();
+ if (!opaqueInfo.isOpaque(fn)) { // It's a normal function
+ List<Expression> auto_reqs = new List<Expression>();
- // First handle all of the requirements' preconditions
- 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
- var body = fn.Body;
- if (opaqueInfo.isOpaque(fn)) { // Opaque functions don't have a body at this point, so use the original body
- body = opaqueInfo.FullVersion(fn).Body;
- }
-
- if (body != null) {
- auto_reqs = generateAutoReqs(body);
-
- if (opaqueInfo.isOpaque(fn)) { // We need to swap fn's variables in for fn_FULL's
- List<Expression> fnVars = new List<Expression>();
- foreach (var formal in fn.Formals) {
- var id = new IdentifierExpr(formal.tok, formal.Name);
- id.Var = formal; // resolve here
- id.Type = formal.Type; // resolve here
- fnVars.Add(id);
- }
+ // First handle all of the requirements' preconditions
+ 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 = generateAutoReqs(fn.Body);
+ fn.Req.AddRange(auto_reqs);
+ addAutoReqToolTipInfo("post", fn, auto_reqs);
+ }
+ } else { // Opaque functions need special handling
+ // The opaque function's requirements are the same as for the _FULL version,
+ // so we don't need to generate them again. We do, however, need to swap
+ // the function's variables for those of the FULL version
+
+ List<Expression> fnVars = new List<Expression>();
+ foreach (var formal in fn.Formals) {
+ var id = new IdentifierExpr(formal.tok, formal.Name);
+ id.Var = formal; // resolve here
+ id.Type = formal.Type; // resolve here
+ fnVars.Add(id);
+ }
- var body_reqs = new List<Expression>();
- foreach (var req in auto_reqs) {
- body_reqs.Add(subVars(opaqueInfo.FullVersion(fn).Formals, fnVars, req, null));
- }
- auto_reqs = body_reqs;
+ var new_reqs = new List<Expression>();
+ foreach (var req in opaqueInfo.FullVersion(fn).Req) {
+ new_reqs.Add(subVars(opaqueInfo.FullVersion(fn).Formals, fnVars, req, null));
}
- fn.Req.AddRange(auto_reqs);
- addAutoReqToolTipInfo("post", fn, auto_reqs);
- }
+ fn.Req.Clear();
+ fn.Req.AddRange(new_reqs);
+ }
}
}
}
|