Skip to content

Commit

Permalink
Fix flaky tests (#2553)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
celinval committed Jun 21, 2023
1 parent 7a111dd commit 43bc890
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 13 deletions.
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
fixed::VecDeque::<u8>::handle_capacity_increase.assertion.7\
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
Status: UNREACHABLE\
Description: "assertion failed: self.head < self.tail"

fixed::VecDeque::<u8>::handle_capacity_increase.assertion.8\
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
Status: UNREACHABLE\
Description: "assertion failed: self.head < self.cap()"

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

fixed::VecDeque::<u8>::handle_capacity_increase.assertion.10\
fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
Status: UNREACHABLE\
Description: "assertion failed: self.cap().count_ones() == 1"

Expand Down
12 changes: 4 additions & 8 deletions tests/expected/object-bits/insufficient/main.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,11 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Checks for error message with an --object-bits value that is too small

// kani-flags: --default-unwind 30 --enable-unstable --cbmc-args --object-bits 5
//! Checks for error message with an --object-bits value that is too small
//! Use linked list to ensure that each member represents a new object.

#[kani::proof]
fn main() {
let mut arr: [i32; 100] = kani::Arbitrary::any_array();
for i in 0..30 {
arr[i] = kani::any();
}
assert!(arr[0] > arr[0] - arr[99]);
let arr: [i32; 18] = kani::Arbitrary::any_array();
std::hint::black_box(std::collections::LinkedList::from(arr));
}
2 changes: 1 addition & 1 deletion tests/ui/should-panic-attribute/expected-panics/expected
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
** 2 of 2 failed\
** 2 of 2 failed
Failed Checks: panicked on the `if` branch!
Failed Checks: panicked on the `else` branch!
VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)

0 comments on commit 43bc890

Please sign in to comment.