Skip to content

Commit 7e62528

Browse files
davidcokdavidcok
davidcok
and
davidcok
authored
Adding tests for more examples in tutorial files (#3197)
<small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> Co-authored-by: davidcok <[email protected]>
1 parent 8428fe7 commit 7e62528

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+376
-209
lines changed

‎.github/workflows/doc-tests.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,5 +59,5 @@ jobs:
5959
- name: Check
6060
run: |
6161
cd dafny/docs
62-
PATH=../bin:$PATH ./check-examples OnlineTutorial/Termination.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
62+
PATH=../bin:$PATH ./check-examples OnlineTutorial/[MLTg]*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
6363
echo Complete

‎docs/OnlineTutorial/Lemmas.1.expect‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
text.dfy(5,0): Error: out-parameter 'index', which is subject to definite-assignment rules, might be uninitialized at this return point
2+
3+
Dafny program verifier finished with 1 verified, 1 error

‎docs/OnlineTutorial/Lemmas.10.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(15,17): Error: A precondition for this call might not hold.
2+
text.dfy(5,35): Related location: This is the precondition that might not hold.
3+
4+
Dafny program verifier finished with 6 verified, 1 error

‎docs/OnlineTutorial/Lemmas.2.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(10,14): Error: This loop invariant might not be maintained by the loop.
2+
text.dfy(10,14): Related message: loop invariant violation
3+
4+
Dafny program verifier finished with 1 verified, 1 error

‎docs/OnlineTutorial/Lemmas.3.expect‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
text.dfy(6,0): Error: A postcondition might not hold on this return path.
2+
text.dfy(5,10): Related location: This is the postcondition that might not hold.
3+
text.dfy(5,56): Related location
4+
text.dfy(5,65): Related location
5+
6+
Dafny program verifier finished with 1 verified, 1 error

‎docs/OnlineTutorial/Lemmas.4.expect‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
text.dfy(6,0): Error: A postcondition might not hold on this return path.
2+
text.dfy(5,10): Related location: This is the postcondition that might not hold.
3+
text.dfy(5,56): Related location
4+
text.dfy(5,65): Related location
5+
6+
Dafny program verifier finished with 3 verified, 1 error

‎docs/OnlineTutorial/Lemmas.5.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(3,0): Error: A postcondition might not hold on this return path.
2+
text.dfy(2,23): Related location: This is the postcondition that might not hold.
3+
4+
Dafny program verifier finished with 1 verified, 1 error

‎docs/OnlineTutorial/Lemmas.6.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(9,9): Error: A postcondition might not hold on this return path.
2+
text.dfy(2,23): Related location: This is the postcondition that might not hold.
3+
4+
Dafny program verifier finished with 1 verified, 1 error

‎docs/OnlineTutorial/Lemmas.7.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(5,0): Error: A postcondition might not hold on this return path.
2+
text.dfy(4,10): Related location: This is the postcondition that might not hold.
3+
4+
Dafny program verifier finished with 4 verified, 1 error

‎docs/OnlineTutorial/Lemmas.8.expect‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
text.dfy(6,0): Error: A postcondition might not hold on this return path.
2+
text.dfy(5,10): Related location: This is the postcondition that might not hold.
3+
4+
Dafny program verifier finished with 4 verified, 1 error

0 commit comments

Comments
 (0)