Merge remote-tracking branch 'fork/main' into history-expressions

.github/workflows/cargo-update.yml

@@ -37,7 +37,7 @@ jobs:
  git diff
  fi
  - name: Create Pull Request
- uses: peter-evans/create-pull-request@v5
+ uses: peter-evans/create-pull-request@v6
  with:
  commit-message: Upgrade cargo dependencies to ${{ env.today }}
  branch: cargo-update-${{ env.today }}

.github/workflows/cbmc-update.yml

@@ -63,7 +63,7 @@ jobs:
 
  - name: Create Pull Request
  if: ${{ env.next_step == 'create_pr' }}
- uses: peter-evans/create-pull-request@v5
+ uses: peter-evans/create-pull-request@v6
  with:
  commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
  branch: cbmc-${{ env.CBMC_LATEST }}

.github/workflows/toolchain-upgrade.yml

@@ -68,7 +68,7 @@ jobs:
  fi
  - name: Create Pull Request
  if: ${{ env.next_step == 'create_pr' }}
- uses: peter-evans/create-pull-request@v5
+ uses: peter-evans/create-pull-request@v6
  with:
  commit-message: Upgrade Rust toolchain to nightly-${{ env.next_toolchain_date }}
  branch: toolchain-${{ env.next_toolchain_date }}

library/kani/src/lib.rs

@@ -288,6 +288,13 @@ macro_rules! cover {
  };
 }
 
+// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
+// crate uses `extern crate std as core`. See
+// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
+#[doc(hidden)]
+#[cfg(not(feature = "concrete_playback"))]
+pub use core::assert as __kani__workaround_core_assert;
+
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
 

library/std/src/lib.rs

@@ -12,13 +12,6 @@
 // re-export all std symbols
 pub use std::*;
 
-// Bind `core::assert` to a different name to avoid possible name conflicts if a
-// crate uses `extern crate std as core`. See
-// https://github.com/model-checking/kani/issues/1949
-#[cfg(not(feature = "concrete_playback"))]
-#[allow(unused_imports)]
-use core::assert as __kani__workaround_core_assert;
-
 #[cfg(not(feature = "concrete_playback"))]
 // Override process calls with stubs.
 pub mod process;
@@ -64,7 +57,7 @@ macro_rules! assert {
  // strategy, which is tracked in
  // https://github.com/model-checking/kani/issues/692
  if false {
- __kani__workaround_core_assert!(true, $($arg)+);
+ kani::__kani__workaround_core_assert!(true, $($arg)+);
  }
  }};
 }
@@ -178,7 +171,7 @@ macro_rules! unreachable {
  // handle.
  ($fmt:expr, $($arg:tt)*) => {{
  if false {
- __kani__workaround_core_assert!(true, $fmt, $($arg)+);
+ kani::__kani__workaround_core_assert!(true, $fmt, $($arg)+);
  }
  kani::panic(concat!("internal error: entered unreachable code: ",
  stringify!($fmt, $($arg)*)))}};
@@ -195,7 +188,7 @@ macro_rules! panic {
  // `panic!("Error message")`
  ($msg:literal $(,)?) => ({
  if false {
- __kani__workaround_core_assert!(true, $msg);
+ kani::__kani__workaround_core_assert!(true, $msg);
  }
  kani::panic(concat!($msg))
  });
@@ -214,7 +207,7 @@ macro_rules! panic {
  // `panic!("Error: {}", code);`
  ($($arg:tt)+) => {{
  if false {
- __kani__workaround_core_assert!(true, $($arg)+);
+ kani::__kani__workaround_core_assert!(true, $($arg)+);
  }
  kani::panic(stringify!($($arg)+));
  }};

tests/ui/extern_std/macro_override.expected

@@ -0,0 +1,15 @@
+Checking harness foo...
+
+Status: SUCCESS\
+Description: ""debug_assert""\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "panic"\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "internal error: entered unreachable code: unreachable"\
+macro_override.rs:
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/ui/extern_std/macro_override.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test if Kani can correctly identify assertions in a no_std crate that re-exports `std` library.
+//! Issue previously reported here: <https://github.com/model-checking/kani/issues/2187>
+//
+// compile-flags: --cfg=feature="std"
+#![no_std]
+
+#[cfg(feature = "std")]
+extern crate std;
+
+#[kani::proof]
+fn foo() {
+ std::debug_assert!(true, "debug_assert");
+ if kani::any_where(|b| !b) {
+ std::unreachable!("unreachable")
+ }
+ if kani::any_where(|val: &u8| *val > 10) < 10 {
+ std::panic!("panic")
+ }
+}