Merge

30 files changed, 566 insertions, 0 deletions

diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy b/Test/dafny0/one-message-per-failed-precondition.dfy
new file mode 100644
index 00000000..ef4f5bd6
--- /dev/null
+++ b/Test/dafny0/one-message-per-failed-precondition.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// When a function call violates two preconditions at the same time, it causes

+// two errors to be reported for the same token

+

+method A(x: int)

+  requires x > 0

+  requires x < 0

+{}

+

+method B(x: int) {

+  A(x);

+}

+

+function fA(x: int): int

+  requires x > 0

+  requires x < 0 { 1 }

+

+function fB(x: int): int { fA(x) }

diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy.expect b/Test/dafny0/one-message-per-failed-precondition.dfy.expect
new file mode 100644
index 00000000..0a76965e
--- /dev/null
+++ b/Test/dafny0/one-message-per-failed-precondition.dfy.expect
@@ -0,0 +1,20 @@
+one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.

+one-message-per-failed-precondition.dfy(9,13): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.

+one-message-per-failed-precondition.dfy(8,13): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition

+one-message-per-failed-precondition.dfy(18,13): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition

+one-message-per-failed-precondition.dfy(17,13): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy
new file mode 100644
index 00000000..67ffe4e4
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file checks that function applications yield trigger candidates

+

+method M(P: (int -> int) -> bool, g: int -> int)

+  requires P.requires(g)

+  requires P(g) {

+  assume forall f: int -> int :: P.requires(f);

+  assume forall f: int -> int :: P(f) ==> f.requires(10) && f(10) == 0;

+  assert forall f: int -> int ::

+    (forall x :: f.requires(x) && g.requires(x) ==> f(x) == g(x)) ==>

+    f.requires(10) ==>

+    f(10) == 0;

+}

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
new file mode 100644
index 00000000..8becae97
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test ensures that the trigger  collector (the routine that picks trigger

+// candidates) does not  actually consider all subsets of terms;  if it did, the

+// following would take horribly long

+

+predicate P0(x: bool)

+predicate P1(x: bool)

+predicate P2(x: bool)

+predicate P3(x: bool)

+predicate P4(x: bool)

+predicate P5(x: bool)

+predicate P6(x: bool)

+predicate P7(x: bool)

+predicate P8(x: bool)

+predicate P9(x: bool)

+predicate P10(x: bool)

+predicate P11(x: bool)

+predicate P12(x: bool)

+predicate P13(x: bool)

+predicate P14(x: bool)

+predicate P15(x: bool)

+predicate P16(x: bool)

+predicate P17(x: bool)

+predicate P18(x: bool)

+predicate P19(x: bool)

+predicate P20(x: bool)

+predicate P21(x: bool)

+predicate P22(x: bool)

+predicate P23(x: bool)

+predicate P24(x: bool)

+predicate P25(x: bool)

+predicate P26(x: bool)

+predicate P27(x: bool)

+predicate P28(x: bool)

+predicate P29(x: bool)

+predicate P30(x: bool)

+predicate P31(x: bool)

+predicate P32(x: bool)

+predicate P33(x: bool)

+predicate P34(x: bool)

+predicate P35(x: bool)

+predicate P36(x: bool)

+predicate P37(x: bool)

+predicate P38(x: bool)

+predicate P39(x: bool)

+predicate P40(x: bool)

+predicate P41(x: bool)

+predicate P42(x: bool)

+predicate P43(x: bool)

+predicate P44(x: bool)

+predicate P45(x: bool)

+predicate P46(x: bool)

+predicate P47(x: bool)

+predicate P48(x: bool)

+predicate P49(x: bool)

+

+method M() {

+  assert forall x :: true || P0(x) || P1(x) || P2(x) || P3(x) || P4(x) || P5(x) || P6(x) || P7(x) || P8(x) || P9(x) || P10(x) || P11(x) || P12(x) || P13(x) || P14(x) || P15(x) || P16(x) || P17(x) || P18(x) || P19(x) || P20(x) || P21(x) || P22(x) || P23(x) || P24(x) || P25(x) || P26(x) || P27(x) || P28(x) || P29(x) || P30(x) || P31(x) || P32(x) || P33(x) || P34(x) || P35(x) || P36(x) || P37(x) || P38(x) || P39(x) || P40(x) || P41(x) || P42(x) || P43(x) || P44(x) || P45(x) || P46(x) || P47(x) || P48(x) || P49(x);

+}

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
new file mode 100644
index 00000000..c90560b0
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 52 verified, 0 errors

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
new file mode 100644
index 00000000..c6722399
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test shows that the loop detection engine makes compromises when looking

+// for subexpressions matching a trigger; in particular, it allows a

+// subexpression to match a trigger without reporting a loop and without being

+// equal to that trigger, as long as the only differences are variable

+

+predicate P(x: int, y: int)

+

+method Test() {

+  // P(x, y) and P(y, x) might look like they would cause a loop. Since they

+  // only differ by their variables, though, they won't raise flags.

+  assume forall x: int, y: int :: P(x, y) == P(y, x);

+

+  // This works independent of extra parentheses:

+  assume forall x: int, y: int :: P(x, y) == (P(y, x));

+

+  // Contrast with the following:

+  assume forall x: int, y: int :: P(x, y) == P(x, y+1);

+}

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
new file mode 100644
index 00000000..29882da7
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -0,0 +1,4 @@
+loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy
new file mode 100644
index 00000000..d5439e09
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file is a series of basic tests for loop detection, focusing on the

+// warnings and information messages

+

+function f(i: int): int

+function g(i: int): int

+

+method M() {

+  assert forall i :: false ==> f(i) == f(f(i));

+  assert forall i :: false ==> f(i) == f(i+1);

+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1);

+

+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == g(i);

+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == f(i);

+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1) && f(i) == f(i);

+

+  assert forall i :: false ==> f(i) == 0;

+  assert forall i :: false ==> f(i+1) == 0;

+  assert forall i {:autotriggers false} :: false ==> f(i+1) == 0;

+

+  assert forall i, j: int :: false ==> f(i) == f(j);

+  assert forall i, j: int :: false ==> f(i) == f(i);

+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j) == 0;

+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j+1) == 0;

+  assert forall i, j: int {:autotriggers false} :: false ==> f(i) == f(i);

+  assert forall i, j: int {:trigger f(i), g(j)} :: false ==> f(i) == f(i);

+}

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
new file mode 100644
index 00000000..1ebc0bce
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -0,0 +1,13 @@
+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:

+   Selected triggers: {f(i)} (loops with {f(i + 1)})

+   (!) Suppressing loops would leave this expression without triggers.

+loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.

+loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.

+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:

+   (!) No trigger covering all quantified variables found.

+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:

+   (!) No trigger covering all quantified variables found.

+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
new file mode 100644
index 00000000..c75cfab9
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This checks that nested quantifiers do get triggers, and that the parent

+// quantifier does not get annotated twice

+

+method M() {

+  ghost var x := forall s: set<int>, x: int :: (x in s ==> forall y :: y == x ==> y in s);

+}

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
new file mode 100644
index 00000000..7423e086
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
@@ -0,0 +1,16 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file shows how Dafny detects loops even for terms that are not literal

+// AST matches. This file also checks that triggers are reported exactly as

+// picked (that is, `x in s` yields `s[x]` for a multiset s), but matches as

+// they appear in the buffer text (that is, `x+1 in s` is not translated to

+// s[x+1] when highlited as a cause for a potential matching loop.

+

+method M() {

+  // This is an obvious loop

+  ghost var b := forall s: multiset<int>, x: int :: s[x] > 0 ==> s[x+1] > 0;

+

+  // x in s loops with s[x+1] due to the way [x in s] is translated

+  ghost var a := forall s: multiset<int>, x: int :: x in s ==> s[x+1] > 0 && x+2 !in s;

+}

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
new file mode 100644
index 00000000..83648626
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -0,0 +1,10 @@
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]})

+ (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:

+   Selected triggers: {s[x]} (loops with {s[x + 1]})

+   (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:

+   Selected triggers: {s[x]} (loops with {x + 2 !in s})

+   (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
new file mode 100644
index 00000000..79a0dc72
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate P(i: int)

+predicate Q(i: int)

+

+/* This file demonstrates a case where automatic trigger splitting is useful to

+   prevent loop detection from reducing expressivity too much. */

+

+lemma exists_0()

+  requires P(0)

+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {

+    // Fails: P(i) is not a trigger

+}

+

+lemma forall_0(i: int)

+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    // Fails: P(i) is not a trigger

+}

+

+

+lemma exists_1()

+  requires P(0)

+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {

+    assert Q(0) || !Q(0);

+    // Works: the dummy assertion introduces a term that causes the quantifier

+    // to trigger, producing a witness.

+  }

+

+lemma forall_1(i: int)

+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    assert Q(i) || !Q(i);

+    // Works: the dummy assertion introduces a term that causes the quantifier

+    // to trigger, producing a witness.

+}

+

+

+lemma exists_2()

+  requires P(0)

+  ensures exists i :: P(i) || (Q(i) ==> P(i+1)) {

+    // Works: automatic trigger splitting allows P(i) to get its own triggers

+}

+

+lemma forall_2(i: int)

+  requires forall j :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    // Works: automatic trigger splitting allows P(i) to get its own triggers

+}

+

+

+lemma loop()

+  requires P(0)

+  requires forall i {:matchingloop} :: i >= 0 ==> Q(i) && (P(i) ==> P(i+1))

+  ensures P(100) {

+    // Works: the matching loop is explicitly allowed

+}

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
new file mode 100644
index 00000000..8d7ff4ef
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -0,0 +1,10 @@
+splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.

+splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+splitting-triggers-recovers-expressivity.dfy(19,15): Error BP5003: A postcondition might not hold on this return path.

+splitting-triggers-recovers-expressivity.dfy(19,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 14 verified, 2 errors

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
new file mode 100644
index 00000000..f25a624e
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.

+

+method f()

+  requires forall y :: y > 0 && y < 0 {

+}

+

+method g(x: int) {

+  f();

+}

+

+function gf(): int

+  requires forall y :: y > 0 && y < 0 {

+    1

+}

+

+function gg(x: int): int {

+  gf()

+}

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
new file mode 100644
index 00000000..c8e1a5fa
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -0,0 +1,32 @@
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,25): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
new file mode 100644
index 00000000..04b8051c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This  file looks  at the  interactions  between inlining  and triggers.   The

+// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on

+// one of the  variables being passed in. Since triggers  are generated prior to

+// inlining  (inlining  happens  during  translation),  inlining  the  last  two

+// instances of that call below would cause  b+1 (a trigger killer) to pop up in

+// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it

+// happen.

+

+function sum(a: int, b: int): int {

+  a + b

+}

+

+predicate sum_is_sum(b: int, c: int) {

+  forall a: int :: sum(a, b) + c == a + b + c

+}

+

+method can_we_inline(b: int, c: int)

+  ensures sum_is_sum(0, 0)     // OK  to inline

+  ensures sum_is_sum(b, c)     // OK  to inline

+  ensures sum_is_sum(b, c+1)   // OK  to inline

+  ensures sum_is_sum(b+1, c)   // NOK to inline

+  ensures sum_is_sum(b+1, c+1) // NOK to inline

+{ }

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
new file mode 100644
index 00000000..16458e41
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file ensures that Dafny does get rid of redundant triggers before

+// annotating a quantifier, and that ths process does not interfere with cycle

+// detection.

+

+function f(x: int): int

+function g(x: int): int

+function h(x: int): int

+

+method M()

+  // In the following, only f(x) is kept. Note that the subset enumeration was

+  // already smart enough to not build any trigger with multiple terms (it only

+  // built 5 candidates)

+  requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0

+

+  // Loop detection still works fine: in the following example, the trigger is

+  // f(f(x))

+  requires forall x: int :: f(x) == f(f(x))

+

+  // This works for multi-triggers, too:

+  requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0

+{

+}

diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
new file mode 100644
index 00000000..6c2c0a2b
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -0,0 +1,17 @@
+useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}

+ Rejected triggers:

+   {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)})

+   {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)})

+   {h(f(x))} (stronger than {f(x)})

+   {g(f(x))} (stronger than {f(x)})

+useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}

+ Rejected triggers: {f(x)} (loops with {f(f(x))})

+useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:

+   {g(f(x)), g(y)}, {f(y), f(x)}

+ Rejected triggers:

+   {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})

+   {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})

+   {g(f(x)), f(y)} (stronger than {f(y), f(x)})

+   {g(f(y)), f(x)} (stronger than {f(y), f(x)})

+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/wishlist/calc.dfy b/Test/wishlist/calc.dfy
new file mode 100644
index 00000000..308fbb9a
--- /dev/null
+++ b/Test/wishlist/calc.dfy
@@ -0,0 +1,17 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// There is a bug in Dafny that causes the error from `L` to be reported at

+// position 0 in this file, instead of on a curly brace.

+

+lemma L()

+  ensures false {

+    calc { true; }

+}

+

+// Empty calc statements work fine, though:

+

+lemma L'()

+  ensures false {

+    calc { }

+}

diff --git a/Test/wishlist/calc.dfy.expect b/Test/wishlist/calc.dfy.expect
new file mode 100644
index 00000000..1d5a55a6
--- /dev/null
+++ b/Test/wishlist/calc.dfy.expect
@@ -0,0 +1,11 @@
+(0,-1): Error BP5003: A postcondition might not hold on this return path.

+calc.dfy(8,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    calc.dfy(9,5): anon2_Else

+calc.dfy(15,16): Error BP5003: A postcondition might not hold on this return path.

+calc.dfy(15,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 2 errors

diff --git a/Test/wishlist/sequences-literals.dfy b/Test/wishlist/sequences-literals.dfy
new file mode 100644
index 00000000..382349a4
--- /dev/null
+++ b/Test/wishlist/sequences-literals.dfy
@@ -0,0 +1,58 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// Note: in the tests below, it could be useful to experiment with the

+// following triggers for some of the library axioms:

+//

+// axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::

+//   { Seq#Contains(s0, x), Seq#Append(s0, s1) }

+//   { Seq#Contains(s1, x), Seq#Append(s0, s1) }

+//   Seq#Contains(Seq#Append(s0, s1), x)

+//      <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));

+//

+// axiom (forall<T> s: Seq T, v: T, x: T ::

+//   { Seq#Contains(s, x), Seq#Build(s, v) }

+//   Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x));

+//

+// Another, not necessarily incompatible approach would be to explicitly add

+// `assume k in s` for each element k of constant lists.

+

+method SmallList() {

+  var s := [0, 1, 5, 6];

+  if * {

+    // This fails: Dafny needs a hint here, because the triggers on the library axioms are pretty strict:

+    assert exists n :: n in s; // WISH

+  } else if * {

+    // This works

+    assert 0 in s;

+    assert exists n :: n in s;

+  } else if * {

+    // This also works, thanks to the magic of triggering on `$Box`.

+    assert exists n {:autotriggers false} :: n in s;

+  }

+}

+

+method LargeList() {

+  var s := [0, 1, 2, 3, 4, 5, 6, 7, 8, /* 9, 10, 11, */ 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, /* 119, 120, 121, */ 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136];

+  if * {

+    // The hint fails here. Maybe because z3 gets into a loop trying to unwrap

+    // this large list? This is also very slow.

+    assert 0 in s; // WISH

+    assert exists n :: n in s;

+  } else if * {

+    // Strangely, the hint works here. Why?

+    assert 122 in s;

+    assert exists n :: n in s;

+  } else if * {

+    // This also fails; since z3 only goes to a depth of 100, this probably

+    // wouldn't work with relaxed triggers eithers

+    assert exists n :: n in s && n >= 120;

+  } else if * {

+    // This works: this is certainly more `triggering-on-$Box` magic, but I'm

+    // not sure exactly how it works

+    assert exists n {:autotriggers false} :: n in s && n >= 120;

+  } else if * {

+    // `$Box` only offers limited solace, though

+    assert exists n {:autotriggers false} :: n in s && n < 3;

+  }

+}

diff --git a/Test/wishlist/sequences-literals.dfy.expect b/Test/wishlist/sequences-literals.dfy.expect
new file mode 100644
index 00000000..18e3f98a
--- /dev/null
+++ b/Test/wishlist/sequences-literals.dfy.expect
@@ -0,0 +1,20 @@
+sequences-literals.dfy(24,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+sequences-literals.dfy(40,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon17_Then

+sequences-literals.dfy(49,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon20_Then

+    (0,0): anon7

+sequences-literals.dfy(56,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon24_Then

+    (0,0): anon15

+

+Dafny program verifier finished with 2 verified, 4 errors

diff --git a/Test/wishlist/sequences-s0-in-s.dfy b/Test/wishlist/sequences-s0-in-s.dfy
new file mode 100644
index 00000000..20127917
--- /dev/null
+++ b/Test/wishlist/sequences-s0-in-s.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// The following is also due to a weakness in the axiomatization: namely, it is

+// not easy to learn, using Dafny's axioms, that s[0] in s. One can of course

+// prove it, but it doesn't come for free.

+

+method InSeqTriggers(s: seq<int>, i: nat)

+  requires forall x :: x in s ==> x > 0;

+  requires |s| > 0 {

+    if * {

+      // Fails

+      assert s[0] > 0; // WISH

+    } else if * {

+      // Works

+      assert s[0] in s;

+      assert s[0] > 0;

+    }

+}

+

+method InSeqNoAutoTriggers(s: seq<int>, i: nat)

+  requires forall x {:autotriggers false} :: x in s ==> x > 0;

+  requires |s| > 0 {

+    assert s[0] > 0; // Works

+}

diff --git a/Test/wishlist/sequences-s0-in-s.dfy.expect b/Test/wishlist/sequences-s0-in-s.dfy.expect
new file mode 100644
index 00000000..4633e5f6
--- /dev/null
+++ b/Test/wishlist/sequences-s0-in-s.dfy.expect
@@ -0,0 +1,6 @@
+sequences-s0-in-s.dfy(13,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+

+Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/wishlist/strings.dfy b/Test/wishlist/strings.dfy
new file mode 100644
index 00000000..372711b0
--- /dev/null
+++ b/Test/wishlist/strings.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method EqualityOfStrings() {

+  assert "a" != "b"; // WISH

+}

diff --git a/Test/wishlist/strings.dfy.expect b/Test/wishlist/strings.dfy.expect
new file mode 100644
index 00000000..2817a66e
--- /dev/null
+++ b/Test/wishlist/strings.dfy.expect
@@ -0,0 +1,5 @@
+strings.dfy(5,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 1 verified, 1 error