diff options
| author |  Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
| commit | 719bf67be5d917a8fe7889c8d131eb27533ca0ff (patch) | |
| tree | 2aa6e95c02b57a00dd33a45f09e9da8b3d2e89cc | |
| parent | e2fa35ca7a769e483014ec03a7c91faf2196f678 (diff) | |
Dafny: fixed translation bug in maps with objects in the domain, added test case
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Maps.dfy | 10 |
3 files changed, 13 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 2758e189..bff09734 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -6087,10 +6087,10 @@ namespace Microsoft.Dafny { var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));
translator.otherTmpVarCount++;
- Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, this);
Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar))
: (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar));
-
+ Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, unboxy, bv.Type, this);
+
Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();
subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 6b7a1079..a0ddd7f1 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1585,7 +1585,7 @@ Maps.dfy(126,13): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 30 verified, 2 errors
+Dafny program verifier finished with 32 verified, 2 errors
-------------------- LiberalEquality.dfy --------------------
LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index a49ac3c1..1c245952 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -180,3 +180,13 @@ method m14() assert u[1] == 1 && u[3] == 4;
assert domain(u) == {0, 1, 3, 4};
}
+
+class A { var x: int; }
+
+method m15(b: set<A>)
+ requires forall a | a in b :: a != null;
+{
+ var m := map a | a in b :: a.x;
+ var aa := new A;
+ assert aa !in m;
+}
\ No newline at end of file |