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 /Test/dafny0/ParseErrors.dfy | |
| parent | 5eed95df25123cb5a335f686b4cb576ce9ca450c (diff) | |
Fixed parsing crash on malformed chaining with == and !!
Diffstat (limited to 'Test/dafny0/ParseErrors.dfy')
| -rw-r--r-- | Test/dafny0/ParseErrors.dfy | 9 |
1 files changed, 9 insertions, 0 deletions
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()
|