Add fixme tests for contracts for different issues

tests/kani/FunctionContracts/fn_params.rs → 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;

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

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());
+}

tests/kani/FunctionContracts/receiver_contracts.rs → 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)]