add markdown tests; test that filepath gets printed

tests/script-based-pre/cargo_list_json/list.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Check that the json file produced by `kani list` is correct.
+# Note that the list.expected file omits the value for "kani-version"
+# to avoid having to update the test every time we bump versions.
+
+output=$(kani list -Z list -Z function-contracts src/lib.rs --format json)
+
+# Check that Kani prints the absolute path to kani-list.json
+absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")"
+expected_last_line="Wrote list results to $absolute_path"
+last_line=$(echo "$output" | tail -n 1)
+
+if [ "$last_line" = "$expected_last_line" ]; then
+    cat kani-list.json
+    exit 0
+else
+    echo "Test failed: Absolute path to kani-list.json is missing from printed output"
+    exit 1
+fi

tests/script-based-pre/cargo_list_md/.gitignore

@@ -0,0 +1 @@
+kani-list.md

tests/script-based-pre/cargo_list_md/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_list"
+version = "0.1.0"
+edition = "2021"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_list_md/kani-list.md

@@ -0,0 +1,14 @@
+
+Contracts:
+|       | Function                      | Contract Harnesses (#[kani::proof_for_contract])               |
+| ----- | ----------------------------- | -------------------------------------------------------------- |
+|       | example::implementation::bar  | example::verify::check_bar                                     |
+|       | example::implementation::foo  | example::verify::check_foo_u32, example::verify::check_foo_u64 |
+|       | example::implementation::func | example::verify::check_func                                    |
+|       | example::prep::parse          | NONE                                                           |
+| Total | 4                             | 4                                                              |
+
+
+Standard Harnesses (#[kani::proof]):
+1. standard_harnesses::example::verify::check_modify
+2. standard_harnesses::example::verify::check_new

tests/script-based-pre/cargo_list_md/list.expected

@@ -0,0 +1,14 @@
+
+Contracts:
+|       | Function                      | Contract Harnesses (#[kani::proof_for_contract])               |
+| ----- | ----------------------------- | -------------------------------------------------------------- |
+|       | example::implementation::bar  | example::verify::check_bar                                     |
+|       | example::implementation::foo  | example::verify::check_foo_u32, example::verify::check_foo_u64 |
+|       | example::implementation::func | example::verify::check_func                                    |
+|       | example::prep::parse          | NONE                                                           |
+| Total | 4                             | 4                                                              |
+
+
+Standard Harnesses (#[kani::proof]):
+1. standard_harnesses::example::verify::check_modify
+2. standard_harnesses::example::verify::check_new

tests/script-based-pre/cargo_list_md/list.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Check that the MD file produced by `kani list` is correct.
+# Note that the list.expected file omits the value for "kani-version"
+# to avoid having to update the test every time we bump versions.
+
+output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown)
+
+# Check that Kani prints the absolute path to kani-list.md
+absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")"
+expected_last_line="Wrote list results to $absolute_path"
+last_line=$(echo "$output" | tail -n 1)
+
+if [ "$last_line" = "$expected_last_line" ]; then
+    cat kani-list.md
+    exit 0
+else
+    echo "Test failed: Absolute path to kani-list.md is missing from printed output"
+    exit 1
+fi

tests/script-based-pre/cargo_list_md/src/lib.rs

@@ -0,0 +1,68 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This test replicates the module structure from the running example in the list RFC.
+//! It ensures that the list command works across modules, and with modifies clauses, history expressions, and generic functions.
+
+mod standard_harnesses;
+
+#[cfg(kani)]
+mod example {
+    mod prep {
+        #[kani::requires(s.len() < 10)]
+        fn parse(s: &str) -> u32 {
+            s.parse().unwrap()
+        }
+    }
+
+    pub mod implementation {
+        #[kani::requires(*x < 4)]
+        #[kani::requires(*x > 2)]
+        #[kani::ensures(|_| old(*x - 1) == *x)]
+        #[kani::ensures(|_| *x == 4)]
+        #[kani::modifies(x)]
+        pub fn bar(x: &mut u32) {
+            *x += 1;
+        }
+
+        #[kani::requires(*x < 100)]
+        #[kani::modifies(x)]
+        pub fn func(x: &mut i32) {
+            *x *= 1;
+        }
+
+        #[kani::requires(true)]
+        #[kani::ensures(|_| old(*x) == *x)]
+        pub fn foo<T: Copy + std::cmp::PartialEq>(x: &mut T) -> T {
+            *x
+        }
+    }
+
+    mod verify {
+        use crate::example::implementation;
+
+        #[kani::proof_for_contract(implementation::bar)]
+        fn check_bar() {
+            let mut x = 7;
+            implementation::bar(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::foo)]
+        fn check_foo_u32() {
+            let mut x: u32 = 7;
+            implementation::foo(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::foo)]
+        fn check_foo_u64() {
+            let mut x: u64 = 7;
+            implementation::foo(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::func)]
+        fn check_func() {
+            let mut x = 7;
+            implementation::func(&mut x);
+        }
+    }
+}

tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Test that the cargo list command can find Kani attributes across multiple files.
+
+#[cfg(kani)]
+mod example {
+    mod verify {
+        #[kani::proof]
+        fn check_modify() {}
+
+        #[kani::proof]
+        fn check_new() {}
+    }
+}

tests/script-based-pre/kani_list_json/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: list.sh
+expected: list.expected

tests/script-based-pre/kani_list_json/list.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Check that the JSON file produced by `kani list` is correct.
+# Note that the list.expected file omits the value for "kani-version"
+# to avoid having to update the test every time we bump versions.
+
+output=$(kani list -Z list -Z function-contracts src/lib.rs --format json)
+
+# Check that Kani prints the absolute path to kani-list.json
+absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")"
+expected_last_line="Wrote list results to $absolute_path"
+last_line=$(echo "$output" | tail -n 1)
+
+if [ "$last_line" = "$expected_last_line" ]; then
+    cat kani-list.json
+    exit 0
+else
+    echo "Test failed: Absolute path to kani-list.json is missing from printed output"
+    exit 1
+fi

tests/script-based-pre/kani_list_md/.gitignore

@@ -0,0 +1 @@
+kani-list.md

tests/script-based-pre/kani_list_md/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: list.sh
+expected: list.expected

tests/script-based-pre/kani_list_md/list.expected

@@ -0,0 +1,14 @@
+
+Contracts:
+|       | Function                      | Contract Harnesses (#[kani::proof_for_contract])               |
+| ----- | ----------------------------- | -------------------------------------------------------------- |
+|       | example::implementation::bar  | example::verify::check_bar                                     |
+|       | example::implementation::foo  | example::verify::check_foo_u32, example::verify::check_foo_u64 |
+|       | example::implementation::func | example::verify::check_func                                    |
+|       | example::prep::parse          | NONE                                                           |
+| Total | 4                             | 4                                                              |
+
+
+Standard Harnesses (#[kani::proof]):
+1. example::verify::check_modify
+2. example::verify::check_new

tests/script-based-pre/kani_list_md/list.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Check that the MD file produced by `kani list` is correct.
+# Note that the list.expected file omits the value for "kani-version"
+# to avoid having to update the test every time we bump versions.
+
+output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown)
+
+# Check that Kani prints the absolute path to kani-list.md
+absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")"
+expected_last_line="Wrote list results to $absolute_path"
+last_line=$(echo "$output" | tail -n 1)
+
+if [ "$last_line" = "$expected_last_line" ]; then
+    cat kani-list.md
+    exit 0
+else
+    echo "Test failed: Absolute path to kani-list.md is missing from printed output"
+    exit 1
+fi

tests/script-based-pre/kani_list_md/src/lib.rs

@@ -0,0 +1,71 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This test replicates the module structure from the running example in the list RFC.
+//! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions.
+
+mod example {
+    mod prep {
+        #[kani::requires(s.len() < 10)]
+        fn parse(s: &str) -> u32 {
+            s.parse().unwrap()
+        }
+    }
+
+    pub mod implementation {
+        #[kani::requires(*x < 4)]
+        #[kani::requires(*x > 2)]
+        #[kani::ensures(|_| old(*x - 1) == *x)]
+        #[kani::ensures(|_| *x == 4)]
+        #[kani::modifies(x)]
+        pub fn bar(x: &mut u32) {
+            *x += 1;
+        }
+
+        #[kani::requires(true)]
+        #[kani::ensures(|_| old(*x) == *x)]
+        pub fn foo<T: Copy + std::cmp::PartialEq>(x: &mut T) -> T {
+            *x
+        }
+
+        #[kani::requires(*x < 100)]
+        #[kani::modifies(x)]
+        pub fn func(x: &mut i32) {
+            *x *= 1;
+        }
+    }
+
+    mod verify {
+        use crate::example::implementation;
+
+        #[kani::proof_for_contract(implementation::bar)]
+        fn check_bar() {
+            let mut x = 7;
+            implementation::bar(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::foo)]
+        fn check_foo_u32() {
+            let mut x: u32 = 7;
+            implementation::foo(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::foo)]
+        fn check_foo_u64() {
+            let mut x: u64 = 7;
+            implementation::foo(&mut x);
+        }
+
+        #[kani::proof_for_contract(implementation::func)]
+        fn check_func() {
+            let mut x = 7;
+            implementation::func(&mut x);
+        }
+
+        #[kani::proof]
+        fn check_modify() {}
+
+        #[kani::proof]
+        fn check_new() {}
+    }
+}