From 5d74b6804431ad81eff2fec7505a85f426f63cbc Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 7 Mar 2023 09:25:59 -0800
Subject: [PATCH] Undo #2194

---
 library/std/src/lib.rs                    | 15 ---------------
 tests/cargo-kani/chrono_dep/Cargo.toml    |  9 +++++++++
 tests/cargo-kani/chrono_dep/main.expected |  1 +
 tests/cargo-kani/chrono_dep/src/main.rs   | 10 ++++++++++
 tests/cargo-kani/no_std/foo.expected      |  2 +-
 tests/cargo-kani/no_std/src/main.rs       |  5 +++--
 6 files changed, 24 insertions(+), 18 deletions(-)
 create mode 100644 tests/cargo-kani/chrono_dep/Cargo.toml
 create mode 100644 tests/cargo-kani/chrono_dep/main.expected
 create mode 100644 tests/cargo-kani/chrono_dep/src/main.rs

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index fbb9da16a4cc..907d98d280a2 100644
--- a/library/std/src/lib.rs
+++ b/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)+));
     }};
diff --git a/tests/cargo-kani/chrono_dep/Cargo.toml b/tests/cargo-kani/chrono_dep/Cargo.toml
new file mode 100644
index 000000000000..5ad240e69e1f
--- /dev/null
+++ b/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"
diff --git a/tests/cargo-kani/chrono_dep/main.expected b/tests/cargo-kani/chrono_dep/main.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/cargo-kani/chrono_dep/main.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/cargo-kani/chrono_dep/src/main.rs b/tests/cargo-kani/chrono_dep/src/main.rs
new file mode 100644
index 000000000000..6b40e78850a2
--- /dev/null
+++ b/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);
+}
diff --git a/tests/cargo-kani/no_std/foo.expected b/tests/cargo-kani/no_std/foo.expected
index 34c886c358cb..7f5175082667 100644
--- a/tests/cargo-kani/no_std/foo.expected
+++ b/tests/cargo-kani/no_std/foo.expected
@@ -1 +1 @@
-VERIFICATION:- SUCCESSFUL
+error: cannot find macro `__kani__workaround_core_assert` in this scope
diff --git a/tests/cargo-kani/no_std/src/main.rs b/tests/cargo-kani/no_std/src/main.rs
index e93b0eaa5d5f..0a2bff90fbd8 100644
--- a/tests/cargo-kani/no_std/src/main.rs
+++ b/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]