From 7cd998145a00c54a25cc46a82f034769b281c4c1 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 14:09:00 -0700 Subject: s/loops with/may loop with/ --- Test/triggers/loop-detection-is-not-too-strict.dfy.expect | 2 +- .../triggers/loop-detection-looks-at-ranges-too.dfy.expect | 4 ++-- .../loop-detection-messages--unit-tests.dfy.expect | 12 ++++++------ .../looping-is-hard-to-decide-modulo-equality.dfy.expect | 4 ++-- Test/triggers/matrix-accesses-are-triggers.dfy.expect | 2 +- .../triggers/old-is-a-special-case-for-triggers.dfy.expect | 10 +++++----- ...rms-do-not-look-like-the-triggers-they-match.dfy.expect | 6 +++--- .../splitting-triggers-recovers-expressivity.dfy.expect | 14 +++++++------- Test/triggers/useless-triggers-are-removed.dfy.expect | 4 ++-- 9 files changed, 29 insertions(+), 29 deletions(-) (limited to 'Test/triggers') 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 270f7e57..6f5ed3d7 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,7 +2,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)}) +loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop 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-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect index 72482de5..ce62d868 100644 --- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -1,6 +1,6 @@ -loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) +loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)}) (!) Suppressing loops would leave this expression without triggers. -loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) +loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 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.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 89d7265c..804a0116 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,21 +1,21 @@ 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)}) + Rejected triggers: {f(i)} (may loop with {f(f(i))}) +loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop 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(13,9): Info: Selected triggers: {f(i)} (may loop 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)}) + Rejected triggers: {f(i)} (may loop 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)}) + Selected triggers: {f(i)} (may loop 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)}) + Selected triggers: {f(i)} (may loop 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)} diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect index c0eebdba..58094110 100644 --- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -1,10 +1,10 @@ looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers: {h(h(c, j), j)}, {h(c, i)}, {c in sc} - Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)}) + Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)}) looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)} Rejected triggers: {g(f(x))} (more specific than {f(x)}) looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect index b9dd1d88..35df02f5 100644 --- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -1,4 +1,4 @@ -matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (loops with {m[j, i + 1]}) +matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]}) (!) Suppressing loops would leave this expression without triggers. matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range Execution trace: diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect index 23ec089d..313d7c16 100644 --- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: {old(f(c))}, {c in sc} old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers: {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc} Rejected triggers: - {g(c)} (loops with {g(f(c))}) - {f(c)} (loops with {f(g(c))}) - {old(g(c))} (loops with {old(g(f(c)))}) - {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))}) + {g(c)} (may loop with {g(f(c))}) + {f(c)} (may loop with {f(g(c))}) + {old(g(c))} (may loop with {old(g(f(c)))}) + {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))}) old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers: {old(f(c))}, {f(c)}, {c in sc} Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))}) 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 index 83648626..f5e47454 100644 --- 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 @@ -1,10 +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]}) +some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop 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]}) + Selected triggers: {s[x]} (may loop 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}) + Selected triggers: {s[x]} (may loop 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.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 63cbc476..58c8dd2b 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,11 +1,11 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)} - Rejected triggers: {P(i)} (loops with {P(i + 1)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop 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)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop with {P(j + 1)}) splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}: Selected triggers: {Q(i)}, {P(i)} @@ -14,19 +14,19 @@ splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i) {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)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop 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)} + {P(i)} (may loop 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/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect index a526e517..2e9bbedf 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy.expect +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} {h(f(x))} (more specific than {f(x)}) {g(f(x))} (more specific 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))}) + Rejected triggers: {f(x)} (may loop 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(y), f(x)} (may loop with {g(f(y))}, {g(f(x))}) {g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)}) {g(f(x)), f(y)} (more specific than {f(y), f(x)}) {g(f(y)), f(x)} (more specific than {f(y), f(x)}) -- cgit v1.2.3