Undo model-checking#2194

library/std/src/lib.rs

@@ -61,14 +61,7 @@ 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)+);
         }
     }};
 }
@@ -172,11 +165,7 @@ 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)*)))}};
@@ -208,11 +197,7 @@ 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/chrono_dep/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "chrono_dep"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+chrono = "=0.4.19"

tests/cargo-kani/chrono_dep/main.expected

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

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

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that the Kani compiler handles chrono crate which was
+//! previously failing due to https://github.com/model-checking/kani/issues/1949
+
+#[kani::proof]
+fn main() {
+    assert!(1 + 1 == 2);
+}

tests/cargo-kani/no_std/foo.expected

@@ -1 +1 @@
-VERIFICATION:- SUCCESSFUL
+error: cannot find macro `__kani__workaround_core_assert` in this scope

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

@@ -1,8 +1,9 @@
 // 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)
+//! This test checks that Kani handles assert in no_std environment which
+//! currently doesn't work:
+//! https://github.com/model-checking/kani/issues/2187)
 
 #![no_std]