diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-23 21:14:19 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-23 21:14:19 -0800 |
| commit | 6c322e2e171ffd46b90981ee28119c2dfb9cd121 (patch) | |
| tree | 70f99769a5f6daf5754fbaec16875dd47b880fe3 | |
| parent | b32bb33052367346817bb8cc6b50943a9ee61c4d (diff) | |
Fix a bug in the interaction between opaque and generics
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 4 |
3 files changed, 7 insertions, 3 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index f8c9c57c..f84ae0b3 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -480,7 +480,7 @@ namespace Microsoft.Dafny List<BoundVar> boundVars = new List<BoundVar>();
foreach (Formal formal in f.Formals) {
- boundVars.Add(new BoundVar(f.tok, formal.Name, formal.Type));
+ boundVars.Add(new BoundVar(f.tok, formal.Name, cloner.CloneType(formal.Type)));
}
// Build the implication connecting the function's requires to the connection with the revealed-body version
@@ -513,7 +513,7 @@ namespace Microsoft.Dafny List<Attributes.Argument/*!*/> argList = new List<Attributes.Argument/*!*/>();
Attributes lemma_attrs = new Attributes("axiom", argList, null);
- var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.IsStatic, f.TypeArgs, new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
+ var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.IsStatic, f.TypeArgs.ConvertAll(cloner.CloneTypeParam), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,
new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, false);
newDecls.Add(reveal);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 804fb1c1..cd2249c7 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1847,7 +1847,7 @@ OpaqueFunctions.dfy(135,12): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 41 verified, 19 errors
+Dafny program verifier finished with 43 verified, 19 errors
-------------------- Maps.dfy --------------------
Maps.dfy(76,8): Error: element may not be in domain
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index 6bff4ef3..d1e27b90 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -151,3 +151,7 @@ module M0 { }
module M1 refines M0 {
}
+
+// ---------------------------------- opaque and generics
+
+function{:opaque} zero<A>():int { 0 }
|