From 0bd765ef68dae7c265751db74246d122003a8962 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 10 Jul 2024 17:37:09 -0400
Subject: [PATCH] change any_modifies back

---
 library/kani/src/internal.rs                     | 16 ----------------
 library/kani/src/lib.rs                          | 15 +++++++++++++++
 .../kani_macros/src/sysroot/contracts/replace.rs | 10 ++--------
 3 files changed, 17 insertions(+), 24 deletions(-)

diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
index 7565520fb820..35550f2895e6 100644
--- a/library/kani/src/internal.rs
+++ b/library/kani/src/internal.rs
@@ -97,22 +97,6 @@ pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
     f(x)
 }
 
-/// This function is only used for function contract instrumentation.
-/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
-/// at compilation time. It allows us to avoid type checking errors while using function
-/// contracts only for verification.
-#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
-#[rustc_diagnostic_item = "KaniAnyModifies"]
-#[inline(never)]
-#[doc(hidden)]
-pub fn any_modifies<T>() -> T {
-    // This function should not be reacheable.
-    // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
-    // otherwise, this might not be properly instantiate. We mark this as unreachable to make
-    // sure Kani doesn't report any false positives.
-    unreachable!()
-}
-
 /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object.
 /// Only for use within function contracts and will not be replaced if the recursive or function stub
 /// replace contracts are not used.
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index dedb32846b2d..6eab2a331811 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -168,6 +168,21 @@ pub fn any<T: Arbitrary>() -> T {
     T::any()
 }
 
+/// This function is only used for function contract instrumentation.
+/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
+/// at compilation time. It allows us to avoid type checking errors while using function
+/// contracts only for verification.
+#[rustc_diagnostic_item = "KaniAnyModifies"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn any_modifies<T>() -> T {
+    // This function should not be reacheable.
+    // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
+    // otherwise, this might not be properly instantiate. We mark this as unreachable to make
+    // sure Kani doesn't report any false positives.
+    unreachable!()
+}
+
 /// This creates a symbolic *valid* value of type `T`.
 /// The value is constrained to be a value accepted by the predicate passed to the filter.
 /// You can assign the return value of this function to a variable that you want to make symbolic.
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
index 852193bce9bb..354d7a01f0b6 100644
--- a/library/kani_macros/src/sysroot/contracts/replace.rs
+++ b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -40,12 +40,7 @@ impl<'a> ContractConditionsHandler<'a> {
         if self.is_first_emit() {
             let return_type = return_type_to_type(&self.annotated_fn.sig.output);
             let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-            (
-                vec![
-                    syn::parse_quote!(let #result : #return_type = kani::internal::any_modifies();),
-                ],
-                vec![],
-            )
+            (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![])
         } else {
             let stmts = &self.annotated_fn.block.stmts;
             let idx = stmts
@@ -157,9 +152,8 @@ fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool {
                 path,
                 attrs,
             })
-            if path.segments.len() == 3
+            if path.segments.len() == 2
             && path.segments[0].ident == "kani"
-            && path.segments[1].ident == "internal"
             && path.segments[2].ident == "any_modifies"
             && attrs.is_empty()
         )