From e3d907f10aa1541dd773533942aa2dcc6f036db5 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 25 Jul 2024 15:45:17 -0700
Subject: [PATCH] Fix tests to include -Zfunction-contracts

Also disable the Arc harness.
---
 tests/kani/FunctionContracts/fn_params.rs          | 1 +
 tests/kani/FunctionContracts/receiver_contracts.rs | 8 ++++++++
 2 files changed, 9 insertions(+)

diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs
index 34b9d54771d6..b485ddf2b32b 100644
--- a/tests/kani/FunctionContracts/fn_params.rs
+++ b/tests/kani/FunctionContracts/fn_params.rs
@@ -4,6 +4,7 @@
 //! Source: <https://doc.rust-lang.org/reference/items/functions.html>
 //!
 //! Note: See `receiver_contracts` for receiver parameters.
+// kani-flags: -Zfunction-contracts
 
 extern crate kani;
 use std::convert::TryFrom;
diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs
index 3a70aff37475..5ca63f1558c3 100644
--- a/tests/kani/FunctionContracts/receiver_contracts.rs
+++ b/tests/kani/FunctionContracts/receiver_contracts.rs
@@ -9,6 +9,7 @@
 //! - Pin<P> where P is one of the types above
 //! Source: <https://doc.rust-lang.org/reference/items/traits.html?highlight=receiver#object-safety>
 // compile-flags: --edition 2021
+// kani-flags: -Zfunction-contracts
 
 #![feature(rustc_attrs)]
 
@@ -63,6 +64,8 @@ impl CharASCII {
         Rc::<_>::get_mut(&mut self).unwrap().0 = new_val
     }
 
+    /// We cannot specify the counter today which is modified in this function.
+    /// <https://github.com/model-checking/kani/issues/3372>
     #[kani::modifies(&self.as_ref().0)]
     #[kani::requires(new_val <= 128)]
     #[kani::ensures(|_| self.as_ref().0 == new_val)]
@@ -121,6 +124,11 @@ mod verify {
         unsafe { Rc::new(obj).set_rc(new_val) };
     }
 
+    /// This test currently fails because we cannot specify that the counter will be modified.
+    /// The counter is behind a pointer, but `Arc` only provide access to the data portion of
+    /// the allocation.
+    /// <https://github.com/model-checking/kani/issues/3372>
+    #[cfg(arc_fails)]
     #[kani::proof_for_contract(CharASCII::set_arc)]
     fn check_arc() {
         let obj = CharASCII::any();