Merge branch 'main' into dependabot/github_actions/peter-evans/create…

…-pull-request-6
model-checking · Feb 6, 2024 · 0eb64ba · 0eb64ba
2 parents ad8a2c2 + 55a7f3e
commit 0eb64ba
Show file tree

Hide file tree

Showing 7 changed files with 48 additions and 48 deletions.
diff --git a/library/kani/src/lib.rs b/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::*;
 

diff --git a/library/std/src/lib.rs b/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)+));
     }};

diff --git a/tests/cargo-kani/no_std/Cargo.toml b/tests/cargo-kani/no_std/Cargo.toml
diff --git a/tests/cargo-kani/no_std/foo.expected b/tests/cargo-kani/no_std/foo.expected
diff --git a/tests/cargo-kani/no_std/src/main.rs b/tests/cargo-kani/no_std/src/main.rs
diff --git a/tests/ui/extern_std/macro_override.expected b/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.
diff --git a/tests/ui/extern_std/macro_override.rs b/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")
+    }
+}