diff options
| author |  leino <unknown> | 2014-10-09 18:36:30 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-09 18:36:30 -0700 |
| commit | db5b38bdaa2aeaf6358aa5f92534ecb4a3d6a0a2 (patch) | |
| tree | 95cbc5d8d9efb21b83e4b087aa2ebe9e3eef453a | |
| parent | 5eed95df25123cb5a335f686b4cb576ce9ca450c (diff) | |
Fixed parsing crash on malformed chaining with == and !!
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/ParseErrors.dfy | 9 | ||||
| -rw-r--r-- | Test/dafny0/ParseErrors.dfy.expect | 16 |
4 files changed, 20 insertions, 9 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2fa2cf88..d60b0b42 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1882,7 +1882,7 @@ RelationalExpression<out Expression e, bool allowSemi, bool allowLambda> if (k != null) {
Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
- } else if (op == BinaryExpr.Opcode.Disjoint) {
+ } else if (op == BinaryExpr.Opcode.Disjoint && acc != null) { // the second conjunct always holds for legal programs
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
} else {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index ad1d5d25..42f8b092 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2946,7 +2946,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (k != null) {
Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
- } else if (op == BinaryExpr.Opcode.Disjoint) {
+ } else if (op == BinaryExpr.Opcode.Disjoint && acc != null) { // the second conjunct always holds for legal programs
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
} else {
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index 17369907..537da50f 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -22,6 +22,15 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set {
}
+method TestChaining2(a: set<int>, b: set<int>, c: set<int>)
+{
+ var x := a !! b !! c;
+ var y := a !! b == c; // error
+ var z0 := a == (b !! c);
+ var z1 := (a == b) !! c;
+ var z2 := a == b !! c; // error: == and !! do not chain together (regression test)
+}
+
// ---------------------- calc statements -----------------------------------
method TestCalc()
diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect index e1acb035..30898479 100644 --- a/Test/dafny0/ParseErrors.dfy.expect +++ b/Test/dafny0/ParseErrors.dfy.expect @@ -6,10 +6,12 @@ ParseErrors.dfy(18,18): error: this operator cannot be part of a chain ParseErrors.dfy(19,19): error: this operator cannot be part of a chain
ParseErrors.dfy(20,18): error: this operator cannot be part of a chain
ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator
-ParseErrors.dfy(49,8): error: the main operator of a calculation must be transitive
-ParseErrors.dfy(65,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(66,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(71,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(72,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(78,2): error: this operator cannot continue this calculation
-14 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(28,19): error: chaining not allowed from the previous operator
+ParseErrors.dfy(31,20): error: can only chain disjoint (!!) with itself.
+ParseErrors.dfy(58,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(74,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(80,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(81,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(87,2): error: this operator cannot continue this calculation
+16 parse errors detected in ParseErrors.dfy
|