Merge branch 'main' into kk-exec-viz

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

@@ -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"
 

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));
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs

@@ -9,5 +9,6 @@
 fn main() {
  let a: i32 = kani::any();
  let b: i32 = kani::any();
- unsafe { std::intrinsics::unchecked_add(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_add(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs

@@ -10,5 +10,6 @@
 fn main() {
  let a: i32 = i32::MIN;
  let b: i32 = -1;
- unsafe { std::intrinsics::unchecked_div(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_div(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs

@@ -10,5 +10,6 @@
 fn main() {
  let a: i32 = kani::any();
  let b: i32 = 0;
- unsafe { std::intrinsics::unchecked_div(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_div(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs

@@ -9,5 +9,6 @@
 fn main() {
  let a: i32 = kani::any();
  let b: i32 = kani::any();
- unsafe { std::intrinsics::unchecked_mul(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_mul(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs

@@ -10,5 +10,6 @@
 fn main() {
  let a: i32 = i32::MIN;
  let b: i32 = -1;
- unsafe { std::intrinsics::unchecked_rem(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_rem(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs

@@ -10,5 +10,6 @@
 fn main() {
  let a: i32 = kani::any();
  let b: i32 = 0;
- unsafe { std::intrinsics::unchecked_rem(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_rem(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs

@@ -9,5 +9,6 @@
 fn main() {
  let a: u32 = kani::any();
  let b: u32 = kani::any();
- unsafe { std::intrinsics::unchecked_shl(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_shl(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs

@@ -9,5 +9,6 @@
 fn main() {
  let a: u32 = kani::any();
  let b: u32 = kani::any();
- unsafe { std::intrinsics::unchecked_shr(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_shr(a, b) });
 }

tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs

@@ -9,5 +9,6 @@
 fn main() {
  let a: i32 = kani::any();
  let b: i32 = kani::any();
- unsafe { std::intrinsics::unchecked_sub(a, b) };
+ // Black box this so it doesn't get pruned by the compiler.
+ std::hint::black_box(unsafe { std::intrinsics::unchecked_sub(a, 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)