Skip to content

Commit

Permalink
Update tests
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Oct 7, 2024
1 parent 4f0b913 commit 421cde4
Show file tree
Hide file tree
Showing 11 changed files with 19 additions and 19 deletions.
4 changes: 2 additions & 2 deletions tests/coverage/abort/expected
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@
14| 1| }\
15| 1| if i == 2 {\
16| | // This should never happen.\
17| 0| process::exit(1);\
18| 1| }\
17| 0| ```process::exit(1)''';\
18| 1| } \
19| | }\
20| 0| ```assert!'''(false, ```"This is unreachable"''');\
21| | }\
2 changes: 1 addition & 1 deletion tests/coverage/assert/expected
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
10| 1| if x < 3 ```{'''\
11| 0| ``` // unreachable'''\
12| 0| ``` assert!(x == 2);'''\
13| 0| ``` }'''\
13| 0| ``` }'''``` '''\
14| 1| } else {\
15| 1| // passes\
16| 1| assert!(x <= 5);\
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/break/expected
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
5| 1| for &num in nums {\
6| | if num > 0 {\
7| 1| return Some(num);\
8| 1| }\
8| 1| } \
9| | }\
10| | // `None` is unreachable because there is at least one positive number.\
11| 0| None\
11| 0| ```None'''\
12| | }\
13| | \
14| | #[kani::proof]\
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/compare/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
3| | \
4| 1| fn compare(x: u16, y: u16) -> u16 {\
5| 1| // The case where `x < y` isn't possible so its region is `UNCOVERED`\
6| 1| if x >= y { 1 } else { 0 }\
6| 1| if x >= y { 1 } else { ```0''' }\
7| | }\
8| | \
9| | #[kani::proof]\
Expand All @@ -12,5 +12,5 @@
12| 1| let y: u16 = kani::any();\
13| 1| if x >= y {\
14| 1| compare(x, y);\
15| 1| }\
15| 1| } \
16| | }\
2 changes: 1 addition & 1 deletion tests/coverage/div-zero/expected
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
3| | \
4| 1| fn div(x: u16, y: u16) -> u16 {\
5| 1| if y != 0 { x / y } else { 0 }\
5| 1| if y != 0 { x / y } else { ```0''' }\
6| | }\
7| | \
8| | #[kani::proof]\
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/early-return/expected
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@
5| 1| for (index, &num) in nums.iter().enumerate() {\
6| | if num == target {\
7| 1| return Some(index);\
8| 1| }\
8| 1| } \
9| | }\
10| 0| None\
10| 0| ```None'''\
11| | }\
12| | \
13| | #[kani::proof]\
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/if-statement/expected
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,9 @@
6| | // The next line is partially covered\
7| 1| if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" }\
8| 0| } else if ```num < 0''' {\
9| 0| "Negative"\
9| 0| ```"Negative"'''\
10| | } else {\
11| 0| "Zero"\
11| 0| ```"Zero"'''\
12| | }\
13| | }\
14| | \
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/known_issues/assert_uncovered_end/expected
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,5 @@
10| 1| let x: u32 = kani::any_where(|val| *val == 5);\
11| 1| if x > 3 {\
12| 1| assert!(x > 4);\
13| 1| }\
13| 1| }``` '''\
14| | }\
8 changes: 4 additions & 4 deletions tests/coverage/known_issues/variant/expected
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,12 @@
16| 1| fn print_direction(dir: Direction) {\
17| | // For some reason, `dir`'s span is reported as `UNCOVERED` too\
18| 0| match ```dir''' {\
19| 0| Direction::Up => println!("Going up!"),\
20| 0| Direction::Down => println!("Going down!"),\
19| 0| Direction::Up => ```println!("Going up!")''',\
20| 0| Direction::Down => ```println!("Going down!")''',\
21| 1| Direction::Left => println!("Going left!"),\
22| 0| Direction::Right if 1 == 1 => println!("Going right!"),\
22| 0| Direction::Right if 1 == ```1 => println!("Going right!")''',\
23| | // This part is unreachable since we cover all variants in the match.\
24| 0| _ => println!("Not going anywhere!"),\
24| 0| _ => ```println!("Not going anywhere!")''',\
25| | }\
26| | }\
27| | \
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/overflow-failure/expected
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
5| | //! arithmetic overflow failure (caused by the second call to `cond_reduce`).\
6| | \
7| 1| fn cond_reduce(thresh: u32, x: u32) -> u32 {\
8| 1| if x > thresh { x - 50 } else { x }\
8| 1| if x > thresh { x - 50 } else { ```x''' }\
9| | }\
10| | \
11| | #[kani::proof]\
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/while-loop-break/expected
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
12| 1| }\
13| 1| index += 1;\
14| | }\
15| 0| None\
15| 0| ```None'''\
16| | }\
17| | \
18| | #[kani::proof]\
Expand Down

0 comments on commit 421cde4

Please sign in to comment.