change any_modifies back

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.

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.

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()
  )