diff options
| author |  Michael Lowell Roberts <mirobert@microsoft.com> | 2015-09-21 13:51:16 -0700 |
|---|---|---|
| committer | Michael Lowell Roberts <mirobert@microsoft.com> | 2015-09-21 13:51:16 -0700 |
| commit | 045c50afc6261beeb83ab4a2f70e597157c9d796 (patch) | |
| tree | ab54452204bd3c3871cada56d06cc34c4c338d1f /Source/Dafny/RefinementTransformer.cs | |
| parent | 96590cb8329d0c902b06d22b6cbecfdbe68cf654 (diff) | |
merged IronDafny updates. two unit tests related to traits do not pass if ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index ba558ea6..24d1126f 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -547,16 +547,16 @@ namespace Microsoft.Dafny if (f is Predicate) {
return new Predicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, isGhost, tps, formals,
- req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
+ req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);
} else if (f is InductivePredicate) {
return new InductivePredicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, tps, formals,
- req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
+ req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);
} else if (f is CoPredicate) {
return new CoPredicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, tps, formals,
- req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
+ req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);
} else {
return new Function(tok, f.Name, f.HasStaticKeyword, f.IsProtected, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),
- req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
+ req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);
}
}
@@ -581,19 +581,19 @@ namespace Microsoft.Dafny var body = newBody ?? refinementCloner.CloneBlockStmt(m.Body);
if (m is Constructor) {
return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
- req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);
} else if (m is InductiveLemma) {
return new InductiveLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
- req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);
} else if (m is CoLemma) {
return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
- req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);
} else if (m is Lemma) {
return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
- req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);
} else {
return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
- req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);
}
}
|