diff options
| author |  qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
| commit | 9c230b0c9037c30879e865aa5b6d994fee5820ff (patch) | |
| tree | 18346dc55e7170c5b2b1663639adfa3444ab2fc0 | |
| parent | d248da33b7763b8c3b2ef75ece9612a45182e7b0 (diff) | |
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
| -rw-r--r-- | Source/Dafny/Translator.cs | 7 | ||||
| -rw-r--r-- | Test/dafny4/Bug73.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny4/Bug73.dfy.expect | 12 |
3 files changed, 30 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index aa3e1854..eac28b05 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -11061,14 +11061,15 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.InMap: {
bool finite = e.E1.Type.AsMapType.Finite;
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
- return Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
+ return Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
BoxIfNecessary(expr.tok, e0, e.E0.Type));
}
case BinaryExpr.ResolvedOpcode.NotInMap: {
bool finite = e.E1.Type.AsMapType.Finite;
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
- return Bpl.Expr.Not(Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
- BoxIfNecessary(expr.tok, e0, e.E0.Type)));
+ Bpl.Expr inMap = Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
+ BoxIfNecessary(expr.tok, e0, e.E0.Type));
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, inMap);
}
case BinaryExpr.ResolvedOpcode.MapDisjoint: {
return translator.FunctionCall(expr.tok, BuiltinFunction.MapDisjoint, null, e0, e1);
diff --git a/Test/dafny4/Bug73.dfy b/Test/dafny4/Bug73.dfy new file mode 100644 index 00000000..c21f818a --- /dev/null +++ b/Test/dafny4/Bug73.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+lemma L(m:map<int, int>, r:int, i:int)
+ requires i != r;
+{
+ assert i in m && i != r;
+}
+
+lemma L2(m:map<int, int>, r:int, i:int)
+ requires i != r;
+{
+ assert i !in m && i != r;
+}
diff --git a/Test/dafny4/Bug73.dfy.expect b/Test/dafny4/Bug73.dfy.expect new file mode 100644 index 00000000..6cf5c156 --- /dev/null +++ b/Test/dafny4/Bug73.dfy.expect @@ -0,0 +1,12 @@ +Bug73.dfy(7,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Bug73.dfy(7,19): anon3_Else
+ (0,0): anon2
+Bug73.dfy(13,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Bug73.dfy(13,20): anon3_Else
+ (0,0): anon2
+
+Dafny program verifier finished with 2 verified, 2 errors
|