From eb7035a075286be2e872943aadfe259e7fac1990 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 14:18:38 -0700 Subject: [PATCH] Fix flaky tests - 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. --- .../reserve_available_capacity_is_no_op.expected | 8 ++++---- tests/expected/object-bits/insufficient/main.rs | 12 ++++-------- .../should-panic-attribute/expected-panics/expected | 2 +- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected index 499ccc7008fc..1b18a4656c4f 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected @@ -1,16 +1,16 @@ -fixed::VecDeque::::handle_capacity_increase.assertion.7\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.head < self.tail" -fixed::VecDeque::::handle_capacity_increase.assertion.8\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.head < self.cap()" -fixed::VecDeque::::handle_capacity_increase.assertion.9\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.tail < self.cap()" -fixed::VecDeque::::handle_capacity_increase.assertion.10\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.cap().count_ones() == 1" diff --git a/tests/expected/object-bits/insufficient/main.rs b/tests/expected/object-bits/insufficient/main.rs index 310ef53667e5..4da74190cb21 100644 --- a/tests/expected/object-bits/insufficient/main.rs +++ b/tests/expected/object-bits/insufficient/main.rs @@ -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)); } diff --git a/tests/ui/should-panic-attribute/expected-panics/expected b/tests/ui/should-panic-attribute/expected-panics/expected index c6a6fa5c6c48..855801a7c0df 100644 --- a/tests/ui/should-panic-attribute/expected-panics/expected +++ b/tests/ui/should-panic-attribute/expected-panics/expected @@ -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)