From aac359fdb4beb60f0f78d4b4e66d27fc6f0601f9 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 26 Jul 2024 15:02:47 -0700
Subject: [PATCH] Add fixme tests for contracts for different issues

---
 .../{fn_params.rs => fixme_fn_params.rs}      |  1 +
 .../fixme_modify_slice_elem.rs                | 25 +++++++++++++++++++
 .../fixme_old_requires_order.rs               | 18 +++++++++++++
 ...ntracts.rs => fixme_receiver_contracts.rs} |  1 +
 4 files changed, 45 insertions(+)
 rename tests/kani/FunctionContracts/{fn_params.rs => fixme_fn_params.rs} (98%)
 create mode 100644 tests/kani/FunctionContracts/fixme_modify_slice_elem.rs
 create mode 100644 tests/kani/FunctionContracts/fixme_old_requires_order.rs
 rename tests/kani/FunctionContracts/{receiver_contracts.rs => fixme_receiver_contracts.rs} (99%)

diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fixme_fn_params.rs
similarity index 98%
rename from tests/kani/FunctionContracts/fn_params.rs
rename to tests/kani/FunctionContracts/fixme_fn_params.rs
index 34b9d54771d6..72714bb0bd20 100644
--- a/tests/kani/FunctionContracts/fn_params.rs
+++ b/tests/kani/FunctionContracts/fixme_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: -Z function-contracts
 
 extern crate kani;
 use std::convert::TryFrom;
diff --git a/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs b/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs
new file mode 100644
index 000000000000..0efdcbdb669b
--- /dev/null
+++ b/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly verify the contract that modifies slices.
+//!
+//! Note that this test used to crash while parsing the annotations.
+// kani-flags: -Zfunction-contracts
+extern crate kani;
+
+#[kani::requires(idx < slice.len())]
+#[kani::modifies(slice.as_ptr().wrapping_add(idx))]
+#[kani::ensures(|_| slice[idx] == new_val)]
+fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) {
+    *slice.get_mut(idx).unwrap() = new_val;
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::modify_slice;
+
+    #[kani::proof_for_contract(modify_slice)]
+    fn check_modify_slice() {
+        let mut data = kani::vec::any_vec::<u32, 5>();
+        modify_slice(&mut data, kani::any(), kani::any())
+    }
+}
diff --git a/tests/kani/FunctionContracts/fixme_old_requires_order.rs b/tests/kani/FunctionContracts/fixme_old_requires_order.rs
new file mode 100644
index 000000000000..c471df44b7e8
--- /dev/null
+++ b/tests/kani/FunctionContracts/fixme_old_requires_order.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that `old()` is executed after the pre-conditions, otherwise it can fail.
+//!
+//! Issue: <https://github.com/model-checking/kani/issues/3370>
+// kani-flags: -Zfunction-contracts
+
+#[kani::requires(val < i32::MAX)]
+#[kani::ensures(|result| *result == old(val + 1))]
+pub fn next(mut val: i32) -> i32 {
+    val + 1
+}
+
+#[kani::proof_for_contract(next)]
+pub fn check_next() {
+    // let _ = next(kani::any_where(|val: &i32| *val < i32::MAX));
+    let _ = next(kani::any());
+}
diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs
similarity index 99%
rename from tests/kani/FunctionContracts/receiver_contracts.rs
rename to tests/kani/FunctionContracts/fixme_receiver_contracts.rs
index 3a70aff37475..22f151c9b240 100644
--- a/tests/kani/FunctionContracts/receiver_contracts.rs
+++ b/tests/kani/FunctionContracts/fixme_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)]