Add test basic cases

tests/expected/function-contract/history/clone_fail.expected

@@ -0,0 +1,11 @@
+error[E0382]: borrow of moved value: `ptr`
+value borrowed here after move\
+move occurs because `ptr` has type `&mut NoCopy<u32>`, which does not implement the `Copy` trait
+
+error[E0382]: borrow of moved value: `ptr`
+#[kani::ensures(old(ptr).0 + 1 == ptr.0)]\
+value moved here
+#[kani::modifies(&mut ptr.0)]\
+value borrowed here after move\
+fn modify(ptr: &mut NoCopy<u32>) {\
+move occurs because `ptr` has type `&mut NoCopy<u32>`, which does not implement the `Copy` trait

tests/expected/function-contract/history/clone_fail.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+struct NoCopy<T>(T);
+
+impl<T: kani::Arbitrary> kani::Arbitrary for NoCopy<T> {
+    fn any() -> Self {
+        Self(kani::any())
+    }
+}
+
+#[kani::ensures(old(ptr).0 + 1 == ptr.0)]
+#[kani::requires(ptr.0 < 100)]
+#[kani::modifies(&mut ptr.0)]
+fn modify(ptr: &mut NoCopy<u32>) {
+    ptr.0 += 1;
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let mut i = kani::any();
+    modify(&mut i);
+}

tests/expected/function-contract/history/clone_pass.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/history/clone_pass.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[derive(Clone)]
+struct NoCopy<T>(T);
+
+impl<T: kani::Arbitrary> kani::Arbitrary for NoCopy<T> {
+    fn any() -> Self {
+        Self(kani::any())
+    }
+}
+
+#[kani::ensures(old(ptr.clone()).0 + 1 == ptr.0)]
+#[kani::requires(ptr.0 < 100)]
+#[kani::modifies(&mut ptr.0)]
+fn modify(ptr: &mut NoCopy<u32>) {
+    ptr.0 += 1;
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let mut i = kani::any();
+    modify(&mut i);
+}

tests/expected/function-contract/history/simple_fail.expected

@@ -0,0 +1,7 @@
+assertion\
+- Status: FAILURE\
+- Description: "old(*ptr) == *ptr"
+
+Failed Checks: old(*ptr) == *ptr
+
+VERIFICATION:- FAILED

tests/expected/function-contract/history/simple_fail.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(old(*ptr) == *ptr)]
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+fn modify(ptr: &mut u32) {
+    *ptr += 1;
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let mut i = kani::any();
+    modify(&mut i);
+}

tests/expected/function-contract/history/simple_pass.expected

@@ -0,0 +1,5 @@
+assertion\
+- Status: SUCCESS\
+- Description: "old(*ptr + 1) == *ptr"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/history/simple_pass.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(old(*ptr + 1) == *ptr)]
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+fn modify(ptr: &mut u32) {
+    *ptr += 1;
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let mut i = kani::any();
+    modify(&mut i);
+}