Fix std overrides in crates where std is used as a feature (rust-lang…

…#2194)

library/std/src/lib.rs

@@ -61,7 +61,14 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
+            #[cfg(not(feature = "std"))]
             __kani__workaround_core_assert!(true, $($arg)+);
+            // In a `no_std` setting where `std` is used as a feature, defining
+            // the alias for `core::assert` doesn't work, so we need to use
+            // `core::assert` directly (see
+            // https://github.com/model-checking/kani/issues/2187)
+            #[cfg(feature = "std")]
+            core::assert!(true, $($arg)+);
         }
     }};
 }
@@ -165,7 +172,11 @@ macro_rules! unreachable {
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
         if false {
+            #[cfg(not(feature = "std"))]
             __kani__workaround_core_assert!(true, $fmt, $($arg)+);
+            // See comment in `assert` definition
+            #[cfg(feature = "std")]
+            core::assert!(true, $fmt, $($arg)+);
         }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
@@ -197,7 +208,11 @@ macro_rules! panic {
     // `panic!("Error: {}", code);`
     ($($arg:tt)+) => {{
         if false {
+            #[cfg(not(feature = "std"))]
             __kani__workaround_core_assert!(true, $($arg)+);
+            // See comment in `assert` definition
+            #[cfg(feature = "std")]
+            core::assert!(true, $($arg)+);
         }
         kani::panic(stringify!($($arg)+));
     }};

tests/cargo-kani/no_std/Cargo.toml

@@ -0,0 +1,16 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "no_std"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+[features]
+std = []
+
+[package.metadata.kani.flags]
+features = ["std"]

tests/cargo-kani/no_std/foo.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/no_std/src/main.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test makes sure Kani handles assert in no_std environment which was
+//! previous failing (see https://github.com/model-checking/kani/issues/2187)
+
+#![no_std]
+
+#[cfg(feature = "std")]
+extern crate std;
+
+#[kani::proof]
+fn foo() {
+    let x: i32 = kani::any();
+    let y = 0;
+    std::debug_assert!(x + y == x, "Message");
+}
+
+fn main() {}