-
Notifications
You must be signed in to change notification settings - Fork 257
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This PR contains 3 minor changes that improve the general build experience. * `.gitignore` is updated to exclude certain files that seem to be generated by the C++ compiler. * The `pre-commit` script that enforces C# coding style is updated to exclude Dafny-generated C# code. * The invisible characters (probably ones that say something about the UTF encoding of text files) at the beginning of some `.expect` files are removed. The tests now pass both through Rider's test mechanisms and through `lit` on the command line. <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>
- Loading branch information
1 parent
df0f713
commit 430d485
Showing
48 changed files
with
51 additions
and
47 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
| ||
|
||
Dafny program verifier finished with 3 verified, 0 errors |
2 changes: 1 addition & 1 deletion
2
...Tests/TestFiles/LitTests/LitTest/proof-obligation-desc/alternative-is-complete.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
array-init-empty.dfy(5,13): Error: unless an initializer is provided for the array elements, a new array of 'T' must have empty size | ||
array-init-empty.dfy(5,13): Error: unless an initializer is provided for the array elements, a new array of 'T' must have empty size | ||
Asserted expression: 1 == 0 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
array-init-size-valid.dfy(5,21): Error: given array size must agree with the number of expressions in the initializing display (0) | ||
array-init-size-valid.dfy(5,21): Error: given array size must agree with the number of expressions in the initializing display (0) | ||
Asserted expression: 1 == |[]| | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...ationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/assignment-shrinks.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
assignment-shrinks.dfy(18,11): Error: an assignment to _new is only allowed to shrink the set | ||
assignment-shrinks.dfy(18,11): Error: an assignment to _new is only allowed to shrink the set | ||
Asserted expression: old(allocated(repeat)) && repeat._new <= old(repeat._new) | ||
|
||
Dafny program verifier finished with 2 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...sts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
char-overflow-unicode.dfy(5,7): Error: char addition might overflow | ||
char-overflow-unicode.dfy(5,7): Error: char addition might overflow | ||
Asserted expression: (0 <= c0 as int + c1 as int && c0 as int + c1 as int < 55296) || (57344 <= c0 as int + c1 as int && c0 as int + c1 as int < 1114112) | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
char-underflow-unicode.dfy(5,7): Error: char subtraction might underflow | ||
char-underflow-unicode.dfy(5,7): Error: char subtraction might underflow | ||
Asserted expression: (0 <= c0 as int - c1 as int && c0 as int - c1 as int < 55296) || (57344 <= c0 as int - c1 as int && c0 as int - c1 as int < 1114112) | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/comprehension-no-alias.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/concurrent-frame-empty.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
conversion-fit.dfy(6,6): Error: value to be converted might not fit in bv8 | ||
conversion-fit.dfy(6,6): Error: value to be converted might not fit in bv8 | ||
Asserted expression: 0 < i && i <= 1 << 8 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
conversion-is-natural.dfy(6,8): Error: value to be converted might be bigger than every natural number | ||
conversion-is-natural.dfy(6,8): Error: value to be converted might be bigger than every natural number | ||
Asserted expression: ord is nat | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
conversion-positive.dfy(6,6): Error: a negative integer cannot be converted to an ORDINAL | ||
conversion-positive.dfy(6,6): Error: a negative integer cannot be converted to an ORDINAL | ||
Asserted expression: 0 <= i | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...tFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
conversion-satisfies-constraints.dfy(8,6): Error: result of operation might violate newtype constraint for 'uint8' | ||
conversion-satisfies-constraints.dfy(8,6): Error: result of operation might violate newtype constraint for 'uint8' | ||
Asserted expression: 0 <= i && i < 256 | ||
|
||
Dafny program verifier finished with 1 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/destructor-valid.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
destructor-valid.dfy(7,13): Error: destructor 'n' can only be applied to datatype values constructed by 'D0' or 'D2' | ||
destructor-valid.dfy(7,13): Error: destructor 'n' can only be applied to datatype values constructed by 'D0' or 'D2' | ||
Asserted expression: d.D0? || d.D2? | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/distinct-lhs.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ensures-stronger.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
for-range-assignable.dfy(6,8): Error: entire range must be assignable to index variable, but some value does not satisfy the subset constraints of 'nat' | ||
for-range-assignable.dfy(6,8): Error: entire range must be assignable to index variable, but some value does not satisfy the subset constraints of 'nat' | ||
Asserted expression: forall i: nat | -1 <= i && i <= 0 :: i is nat | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
for-range-bounds-valid.dfy(6,13): Error: lower bound must not exceed upper bound | ||
for-range-bounds-valid.dfy(6,13): Error: lower bound must not exceed upper bound | ||
Asserted expression: 1 <= 0 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-lhs-unique.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/frame-dereference-non-null.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
frame-dereference-non-null.dfy(7,12): Error: frame expression might dereference null | ||
frame-dereference-non-null.dfy(7,12): Error: frame expression might dereference null | ||
Asserted expression: c != null | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/function-contract-override.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/indices-in-domain.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
is-allocated.dfy(11,19): Error: receiver could not be proved to be allocated in the state in which its fields are accessed | ||
is-allocated.dfy(11,19): Error: receiver could not be proved to be allocated in the state in which its fields are accessed | ||
Asserted expression: old(allocated(c)) | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
is-integer.dfy(6,6): Error: the real-based number must be an integer (if you want truncation, apply .Floor to the real-based number) | ||
is-integer.dfy(6,6): Error: the real-based number must be an integer (if you want truncation, apply .Floor to the real-based number) | ||
Asserted expression: r == r.Floor as real | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/loop-invariant.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/match-is-complete.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
non-negative.dfy(6,8): Error: sequence size might be negative | ||
non-negative.dfy(6,8): Error: sequence size might be negative | ||
Asserted expression: 0 <= -1 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
non-null.dfy(6,6): Error: target object might be null | ||
non-null.dfy(6,6): Error: target object might be null | ||
Asserted expression: a != null | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/not-ghost-variant.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...estFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
ordinal-subtraction-is-natural.dfy(7,7): Error: RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger | ||
ordinal-subtraction-is-natural.dfy(7,7): Error: RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger | ||
Asserted expression: o1.IsNat | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
ordinal-subtraction-underflow.dfy(7,7): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large) | ||
ordinal-subtraction-underflow.dfy(7,7): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large) | ||
Asserted expression: o1.Offset <= o0.Offset | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/pattern-shape-is-valid.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
pattern-shape-is-valid.dfy(7,11): Error: assertion might not hold | ||
pattern-shape-is-valid.dfy(7,11): Error: assertion might not hold | ||
Asserted expression: d.D0? | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/precondition-satisfied.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/prefix-equality-limit.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
prefix-equality-limit.dfy(7,19): Error: prefix-equality limit must be at least 0 | ||
prefix-equality-limit.dfy(7,19): Error: prefix-equality limit must be at least 0 | ||
Asserted expression: 0 <= i | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/requires-weaker.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative | ||
shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative | ||
Asserted expression: 0 <= -1 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
shift-upper-bound.dfy(5,6): Error: rotate amount must not exceed the width of the result (2) | ||
shift-upper-bound.dfy(5,6): Error: rotate amount must not exceed the width of the result (2) | ||
Asserted expression: 3 <= 2 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...s/LitTests/LitTest/proof-obligation-desc/subrange-check-no-type-system-refresh.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/subrange-check.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...Tests/TestFiles/LitTests/LitTest/proof-obligation-desc/valid-constructor-names.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
valid-constructor-names.dfy(7,14): Error: source of datatype update must be constructed by 'D2' or 'D0' | ||
valid-constructor-names.dfy(7,14): Error: source of datatype update must be constructed by 'D2' or 'D0' | ||
Asserted expression: d.D2? || d.D0? | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect
100644 → 100755
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
witness-check.dfy(4,8): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type | ||
witness-check.dfy(4,8): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type | ||
Asserted expression: 0 > 0 | ||
|
||
Dafny program verifier finished with 0 verified, 1 error |
2 changes: 1 addition & 1 deletion
2
...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/yield-ensures.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters