Add /printTooltips to trigger tests

17 files changed, 87 insertions, 10 deletions

diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy
index 67ffe4e4..0aad9018 100644
--- a/Test/triggers/function-applications-are-triggers.dfy
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

 // This file checks that function applications yield trigger candidates

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 069e7767..7922e88d 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -1,2 +1,13 @@
+function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}

+function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f.requires(10)}:

+   Selected triggers:

+     {f(10)}, {f.requires(10)}, {P(f)}

+function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(10) == 0}:

+   Selected triggers:

+     {f(10)}, {f.requires(10)}, {P(f)}

+function-applications-are-triggers.dfy(11,9): Info: Selected triggers:

+   {f(10)}, {f.requires(10)}

+function-applications-are-triggers.dfy(12,5): Info: Selected triggers:

+   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}

 

 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
index 8becae97..58eb56e1 100644
--- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
index c90560b0..5e7c14b9 100644
--- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -1,2 +1,4 @@
+large-quantifiers-dont-break-dafny.dfy(60,9): Info: Selected triggers:

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

 

 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
index c6722399..a5a30c81 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 29882da7..270f7e57 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -1,3 +1,7 @@
+loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers:

+   {P(y, x)}, {P(x, y)}

+loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:

+   {P(y, x)}, {P(x, y)}

 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.

 

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy
index d5439e09..c1560317 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
index 1ebc0bce..89d7265c 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -1,13 +1,37 @@
+loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}

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

 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(13,9): Info: Selected triggers: {f(i)} (loops with {f(i + 1)})

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

+   Selected triggers: {g(i)}

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

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

+   Selected triggers:

+     {g(i)}, {f(i)}

 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(16,9): Info: For expression {false ==> f(i) == f(i)}:

+   Selected triggers: {f(i)}

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

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

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

+   Selected triggers: {f(i)}

+loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}

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

+loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for {false ==> f(i + 1) == 0}.

+loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)}

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

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

+   Selected triggers: {g(j), f(i)}

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

+   Selected triggers: {g(j), f(i)}

 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.

+loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.

+loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.

 

 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
index c75cfab9..a55019db 100644
--- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
index 069e7767..172f5607 100644
--- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -1,2 +1,4 @@
+nested-quantifiers-all-get-triggers.dfy(8,17): Info: Selected triggers: {x in s}

+nested-quantifiers-all-get-triggers.dfy(8,59): Info: Selected triggers: {y in s}

 

 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
index 7423e086..d7636ea2 100644
--- 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
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
index 79a0dc72..dd1bd81d 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

 predicate P(i: int)

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
index 8d7ff4ef..63cbc476 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -1,3 +1,32 @@
+splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}

+ Rejected triggers: {P(i)} (loops with {P(i + 1)})

+splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}

+ Rejected triggers: {P(j)} (loops with {P(j + 1)})

+splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}

+ Rejected triggers: {P(i)} (loops with {P(i + 1)})

+splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}

+ Rejected triggers: {P(j)} (loops with {P(j + 1)})

+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:

+   Selected triggers:

+     {Q(i)}, {P(i)}

+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)}:

+   Selected triggers:

+     {Q(i)}, {P(i)}

+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:

+   Selected triggers: {Q(i)}

+   Rejected triggers: {P(i)} (loops with {P(i + 1)})

+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:

+   Selected triggers:

+     {Q(j)}, {P(j)}

+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:

+   Selected triggers: {Q(j)}

+   Rejected triggers: {P(j)} (loops with {P(j + 1)})

+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:

+   Selected triggers:

+     {P(i)}, {Q(i)}

+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:

+   Selected triggers:

+     {P(i)} (loops with {P(i + 1)}), {Q(i)}

 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:

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
index f25a624e..20e90843 100644
--- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%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.

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
index 04b8051c..90af62a3 100644
--- a/Test/triggers/triggers-prevent-some-inlining.dfy
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
index 73ba063c..4c24893e 100644
--- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -1,2 +1,7 @@
+triggers-prevent-some-inlining.dfy(17,2): Info: Selected triggers: {sum(a, b)}

+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.

+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.

+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.

+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.

 

 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
index 16458e41..658890f2 100644
--- a/Test/triggers/useless-triggers-are-removed.dfy
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

 

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