Skip to content

Commit 43bc890

Browse files
authored
Fix flaky tests (#2553)
This PR fixes a few flaky tests that started to fail in the ongoing toolchain update (#2551) - The object bits test itself doesn't create that many objects since an array is represented as the same allocated object. Use LinkedList instead. - Do not rely on property number. - Do not rely on the order that failed checks is printed.
1 parent 7a111dd commit 43bc890

File tree

3 files changed

+9
-13
lines changed

3 files changed

+9
-13
lines changed

tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
1-
fixed::VecDeque::<u8>::handle_capacity_increase.assertion.7\
1+
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
22
Status: UNREACHABLE\
33
Description: "assertion failed: self.head < self.tail"
44

5-
fixed::VecDeque::<u8>::handle_capacity_increase.assertion.8\
5+
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
66
Status: UNREACHABLE\
77
Description: "assertion failed: self.head < self.cap()"
88

9-
fixed::VecDeque::<u8>::handle_capacity_increase.assertion.9\
9+
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
1010
Status: UNREACHABLE\
1111
Description: "assertion failed: self.tail < self.cap()"
1212

13-
fixed::VecDeque::<u8>::handle_capacity_increase.assertion.10\
13+
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
1414
Status: UNREACHABLE\
1515
Description: "assertion failed: self.cap().count_ones() == 1"
1616

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,11 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
4-
// Checks for error message with an --object-bits value that is too small
5-
63
// kani-flags: --default-unwind 30 --enable-unstable --cbmc-args --object-bits 5
4+
//! Checks for error message with an --object-bits value that is too small
5+
//! Use linked list to ensure that each member represents a new object.
76
87
#[kani::proof]
98
fn main() {
10-
let mut arr: [i32; 100] = kani::Arbitrary::any_array();
11-
for i in 0..30 {
12-
arr[i] = kani::any();
13-
}
14-
assert!(arr[0] > arr[0] - arr[99]);
9+
let arr: [i32; 18] = kani::Arbitrary::any_array();
10+
std::hint::black_box(std::collections::LinkedList::from(arr));
1511
}
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
** 2 of 2 failed\
1+
** 2 of 2 failed
22
Failed Checks: panicked on the `if` branch!
33
Failed Checks: panicked on the `else` branch!
44
VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)

0 commit comments

Comments
 (0)