Merge pull request #29 from os-checker/test-proof-for-contract

Test: support of `#[kani::proof_for_contract]`

Author: zjp-CN

tests/proofs.rs

@@ -14,11 +14,13 @@ fn test_proofs() -> eyre::Result<()> {
         }
     }
 
+    proofs.sort();
     expect![[r#"
         [
-            "tests/proofs/standard_proofs_with_contracts.rs",
-            "tests/proofs/standard_proofs.rs",
             "tests/proofs/ad_hoc.rs",
+            "tests/proofs/proofs_for_contract.rs",
+            "tests/proofs/standard_proofs.rs",
+            "tests/proofs/standard_proofs_with_contracts.rs",
         ]
     "#]]
     .assert_debug_eq(&proofs);

tests/proofs/proofs_for_contract.rs

@@ -0,0 +1,38 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::requires(a > 0)]
+    fn contract_requires(a: u8) {}
+
+    #[kani::proof_for_contract(contract_requires)]
+    fn single_contract_requires() {
+        contract_requires(0);
+    }
+
+    #[kani::ensures(|&ret| ret > 0)]
+    fn contract_ensures(a: u8) -> u8 {
+        a
+    }
+
+    #[kani::proof_for_contract(contract_ensures)]
+    fn single_with_contract_ensures() {
+        contract_ensures(0);
+    }
+
+    #[kani::proof_for_contract(contract_requires)]
+    fn two_contracts_requires_and_ensures() {
+        let val = contract_ensures(0);
+        contract_requires(val);
+    }
+
+    #[kani::requires(a > 0)]
+    #[kani::ensures(|&ret| ret > 0)]
+    fn contract(a: u8) -> u8 {
+        a
+    }
+
+    #[kani::proof_for_contract(contract)]
+    fn single_contract() {
+        let val = contract(1);
+        assert!(val > 0);
+    }
+}

tests/proofs/standard_proofs_with_contracts.rs

@@ -21,7 +21,7 @@ mod verify {
     #[kani::proof]
     fn two_contracts_requires_and_ensures() {
         let val = contract_ensures(0);
-        contract_ensures(val);
+        contract_requires(val);
     }
 
     #[kani::requires(a > 0)]