Complete blessing for coverage tests

tests/coverage/abort/expected

@@ -1,22 +1,21 @@
-/home/ubuntu/kani/tests/coverage/abort/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| | //! Test that the abort() function is respected and nothing beyond it will execute.
- 5| | 
- 6| | use std::process;
- 7| | 
- 8| | #[kani::proof]
- 9| 2| fn main() {
- 10| 2| for i in 0..4 {
- 11| | if i == 1 {
- 12| | // This comes first and it should be reachable.
- 13| 2| process::abort();
- 14| 2| }
- 15| 2| if i == 2 {
- 16| | // This should never happen.
- 17| 0| process::exit(1);
- 18| 2| }
- 19| | }
- 20| 0| ```assert!'''(false, ```"This is unreachable"''');
- 21| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | //! Test that the abort() function is respected and nothing beyond it will execute.\
+ 5| | \
+ 6| | use std::process;\
+ 7| | \
+ 8| | #[kani::proof]\
+ 9| 2| fn main() {\
+ 10| 2| for i in 0..4 {\
+ 11| | if i == 1 {\
+ 12| | // This comes first and it should be reachable.\
+ 13| 2| process::abort();\
+ 14| 2| }\
+ 15| 2| if i == 2 {\
+ 16| | // This should never happen.\
+ 17| 0| process::exit(1);\
+ 18| 2| }\
+ 19| | }\
+ 20| 0| ```assert!'''(false, ```"This is unreachable"''');\
+ 21| | }\

tests/coverage/assert/expected

@@ -1,19 +1,18 @@
-/home/ubuntu/kani/tests/coverage/assert/test.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| | #[kani::proof]
- 5| 2| fn foo() {
- 6| 2| let x: i32 = kani::any();
- 7| 2| if x > 5 {
- 8| | // fails
- 9| 2| assert!(x < 4);
- 10| 2| if x < 3 ```{'''
- 11| 0| ``` // unreachable'''
- 12| 0| ``` assert!(x == 2);'''
- 13| 0| ``` }'''
- 14| 2| } else {
- 15| 2| // passes
- 16| 2| assert!(x <= 5);
- 17| 2| }
- 18| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn foo() {\
+ 6| 2| let x: i32 = kani::any();\
+ 7| 2| if x > 5 {\
+ 8| | // fails\
+ 9| 2| assert!(x < 4);\
+ 10| 2| if x < 3 ```{'''\
+ 11| 0| ``` // unreachable'''\
+ 12| 0| ``` assert!(x == 2);'''\
+ 13| 0| ``` }'''\
+ 14| 2| } else {\
+ 15| 2| // passes\
+ 16| 2| assert!(x <= 5);\
+ 17| 2| }\
+ 18| | }\

tests/coverage/assert_eq/expected

@@ -1,12 +1,11 @@
-/home/ubuntu/kani/tests/coverage/assert_eq/test.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| | #[kani::proof]
- 5| 2| fn main() {
- 6| 2| let x: i32 = kani::any();
- 7| 2| let y = if x > 10 { 15 } else { 33 };
- 8| 0| if y > 50 ```{'''
- 9| 0| ``` assert_eq!(y, 55);'''
- 10| 2| ``` }'''
- 11| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn main() {\
+ 6| 2| let x: i32 = kani::any();\
+ 7| 2| let y = if x > 10 { 15 } else { 33 };\
+ 8| 0| if y > 50 ```{'''\
+ 9| 0| ``` assert_eq!(y, 55);'''\
+ 10| 2| ``` }'''\
+ 11| | }\

tests/coverage/assert_ne/expected

@@ -1,15 +1,14 @@
-/home/ubuntu/kani/tests/coverage/assert_ne/test.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| | #[kani::proof]
- 5| 2| fn main() {
- 6| 2| let x: u32 = kani::any();
- 7| 2| if x > 0 {
- 8| 2| let y = x / 2;
- 9| 2| // y is strictly less than x
- 10| 2| if y == x ```{'''
- 11| 0| ``` assert_ne!(y, 1);'''
- 12| 2| ``` }'''
- 13| 2| }
- 14| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn main() {\
+ 6| 2| let x: u32 = kani::any();\
+ 7| 2| if x > 0 {\
+ 8| 2| let y = x / 2;\
+ 9| 2| // y is strictly less than x\
+ 10| 2| if y == x ```{'''\
+ 11| 0| ``` assert_ne!(y, 1);'''\
+ 12| 2| ``` }'''\
+ 13| 2| }\
+ 14| | }\

tests/coverage/break/expected

@@ -1,20 +1,19 @@
-/home/ubuntu/kani/tests/coverage/break/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| 2| fn find_positive(nums: &[i32]) -> Option<i32> {
- 5| 2| for &num in nums {
- 6| | if num > 0 {
- 7| 2| return Some(num);
- 8| 2| }
- 9| | }
- 10| | // `None` is unreachable because there is at least one positive number.
- 11| 0| None
- 12| | }
- 13| | 
- 14| | #[kani::proof]
- 15| 2| fn main() {
- 16| 2| let numbers = [-3, -1, 0, 2, 4];
- 17| 2| let result = find_positive(&numbers);
- 18| 2| assert_eq!(result, Some(2));
- 19| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn find_positive(nums: &[i32]) -> Option<i32> {\
+ 5| 2| for &num in nums {\
+ 6| | if num > 0 {\
+ 7| 2| return Some(num);\
+ 8| 2| }\
+ 9| | }\
+ 10| | // `None` is unreachable because there is at least one positive number.\
+ 11| 0| None\
+ 12| | }\
+ 13| | \
+ 14| | #[kani::proof]\
+ 15| 2| fn main() {\
+ 16| 2| let numbers = [-3, -1, 0, 2, 4];\
+ 17| 2| let result = find_positive(&numbers);\
+ 18| 2| assert_eq!(result, Some(2));\
+ 19| | }\

tests/coverage/compare/expected

@@ -1,17 +1,16 @@
-/home/ubuntu/kani/tests/coverage/compare/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| 2| fn compare(x: u16, y: u16) -> u16 {
- 5| 2| // The case where `x < y` isn't possible so its region is `UNCOVERED`
- 6| 2| if x >= y { 1 } else { 0 }
- 7| | }
- 8| | 
- 9| | #[kani::proof]
- 10| 2| fn main() {
- 11| 2| let x: u16 = kani::any();
- 12| 2| let y: u16 = kani::any();
- 13| 2| if x >= y {
- 14| 2| compare(x, y);
- 15| 2| }
- 16| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn compare(x: u16, y: u16) -> u16 {\
+ 5| 2| // The case where `x < y` isn't possible so its region is `UNCOVERED`\
+ 6| 2| if x >= y { 1 } else { 0 }\
+ 7| | }\
+ 8| | \
+ 9| | #[kani::proof]\
+ 10| 2| fn main() {\
+ 11| 2| let x: u16 = kani::any();\
+ 12| 2| let y: u16 = kani::any();\
+ 13| 2| if x >= y {\
+ 14| 2| compare(x, y);\
+ 15| 2| }\
+ 16| | }\

tests/coverage/contradiction/expected

@@ -1,15 +1,14 @@
-/home/ubuntu/kani/tests/coverage/contradiction/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | #[kani::proof]
- 4| 2| fn contradiction() {
- 5| 2| let x: u8 = kani::any();
- 6| 2| let mut y: u8 = 0;
- 7| 2| if x > 5 {
- 8| 2| if x < 2 ```{'''
- 9| 0| ``` y = x;'''
- 10| 2| ``` }'''
- 11| 2| } else {
- 12| 2| assert!(x < 10);
- 13| 2| }
- 14| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | #[kani::proof]\
+ 4| 2| fn contradiction() {\
+ 5| 2| let x: u8 = kani::any();\
+ 6| 2| let mut y: u8 = 0;\
+ 7| 2| if x > 5 {\
+ 8| 2| if x < 2 ```{'''\
+ 9| 0| ``` y = x;'''\
+ 10| 2| ``` }'''\
+ 11| 2| } else {\
+ 12| 2| assert!(x < 10);\
+ 13| 2| }\
+ 14| | }\

tests/coverage/debug-assert/expected

@@ -1,16 +1,15 @@
-/home/ubuntu/kani/tests/coverage/debug-assert/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| | //! This test checks that the regions after the `debug_assert` macro are
- 5| | //! `UNCOVERED`. In fact, for this example, the region associated to `"This
- 6| | //! should fail and stop the execution"` is also `UNCOVERED` because the macro
- 7| | //! calls span two regions each.
- 8| | 
- 9| | #[kani::proof]
- 10| 2| fn main() {
- 11| 2| for i in 0..4 {
- 12| 0| debug_assert!(i > 0, ```"This should fail and stop the execution"''');
- 13| 0| ```assert!(i == 0''', ```"This should be unreachable"''');
- 14| | }
- 15| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | //! This test checks that the regions after the `debug_assert` macro are\
+ 5| | //! `UNCOVERED`. In fact, for this example, the region associated to `"This\
+ 6| | //! should fail and stop the execution"` is also `UNCOVERED` because the macro\
+ 7| | //! calls span two regions each.\
+ 8| | \
+ 9| | #[kani::proof]\
+ 10| 2| fn main() {\
+ 11| 2| for i in 0..4 {\
+ 12| 0| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
+ 13| 0| ```assert!(i == 0''', ```"This should be unreachable"''');\
+ 14| | }\
+ 15| | }\

tests/coverage/div-zero/expected

@@ -1,12 +1,11 @@
-/home/ubuntu/kani/tests/coverage/div-zero/test.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| 2| fn div(x: u16, y: u16) -> u16 {
- 5| 2| if y != 0 { x / y } else { 0 }
- 6| | }
- 7| | 
- 8| | #[kani::proof]
- 9| 2| fn main() {
- 10| 2| div(11, 3);
- 11| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn div(x: u16, y: u16) -> u16 {\
+ 5| 2| if y != 0 { x / y } else { 0 }\
+ 6| | }\
+ 7| | \
+ 8| | #[kani::proof]\
+ 9| 2| fn main() {\
+ 10| 2| div(11, 3);\
+ 11| | }\

tests/coverage/early-return/expected

@@ -1,20 +1,19 @@
-/home/ubuntu/kani/tests/coverage/early-return/main.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | 
- 4| 2| fn find_index(nums: &[i32], target: i32) -> Option<usize> {
- 5| 2| for (index, &num) in nums.iter().enumerate() {
- 6| | if num == target {
- 7| 2| return Some(index);
- 8| 2| }
- 9| | }
- 10| 0| None
- 11| | }
- 12| | 
- 13| | #[kani::proof]
- 14| 2| fn main() {
- 15| 2| let numbers = [10, 20, 30, 40, 50];
- 16| 2| let target = 30;
- 17| 2| let result = find_index(&numbers, target);
- 18| 2| assert_eq!(result, Some(2));
- 19| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
+ 5| 2| for (index, &num) in nums.iter().enumerate() {\
+ 6| | if num == target {\
+ 7| 2| return Some(index);\
+ 8| 2| }\
+ 9| | }\
+ 10| 0| None\
+ 11| | }\
+ 12| | \
+ 13| | #[kani::proof]\
+ 14| 2| fn main() {\
+ 15| 2| let numbers = [10, 20, 30, 40, 50];\
+ 16| 2| let target = 30;\
+ 17| 2| let result = find_index(&numbers, target);\
+ 18| 2| assert_eq!(result, Some(2));\
+ 19| | }\

tests/coverage/if-statement-multi/expected

@@ -1,27 +1,26 @@
-/home/ubuntu/kani/tests/coverage/if-statement-multi/test.rs
- 1| | // Copyright Kani Contributors
- 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT
- 3| | // kani-flags: --coverage -Zsource-coverage
- 4| | 
- 5| | //! Checks that we are covering all regions except
- 6| | //! * the `val == 42` condition
- 7| | //! * the `false` branch
- 8| | //!
- 9| | //! No coverage information is shown for `_other_function` because it's sliced
- 10| | //! off: <https://github.com/model-checking/kani/issues/3445>
- 11| | 
- 12| 0| ```fn _other_function() {'''
- 13| 0| ``` println!("Hello, world!");'''
- 14| 0| ```}'''
- 15| | 
- 16| 2| fn test_cov(val: u32) -> bool {
- 17| 2| if val < 3 || ```val == 42''' { true } else { ```false''' }
- 18| | }
- 19| | 
- 20| | #[cfg_attr(kani, kani::proof)]
- 21| 2| fn main() {
- 22| 2| let test1 = test_cov(1);
- 23| 2| let test2 = test_cov(2);
- 24| 2| assert!(test1);
- 25| 2| assert!(test2);
- 26| | }
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | // kani-flags: --coverage -Zsource-coverage\
+ 4| | \
+ 5| | //! Checks that we are covering all regions except\
+ 6| | //! * the `val == 42` condition\
+ 7| | //! * the `false` branch\
+ 8| | //!\
+ 9| | //! No coverage information is shown for `_other_function` because it's sliced\
+ 10| | //! off: <https://github.com/model-checking/kani/issues/3445>\
+ 11| | \
+ 12| 0| ```fn _other_function() {'''\
+ 13| 0| ``` println!("Hello, world!");'''\
+ 14| 0| ```}'''\
+ 15| | \
+ 16| 2| fn test_cov(val: u32) -> bool {\
+ 17| 2| if val < 3 || ```val == 42''' { true } else { ```false''' }\
+ 18| | }\
+ 19| | \
+ 20| | #[cfg_attr(kani, kani::proof)]\
+ 21| 2| fn main() {\
+ 22| 2| let test1 = test_cov(1);\
+ 23| 2| let test2 = test_cov(2);\
+ 24| 2| assert!(test1);\
+ 25| 2| assert!(test2);\
+ 26| | }\