add tests that autoharness does not generate harnesses for functions outside the local crate

Author: Carolyn Zech

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

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "cargo_autoharness_dependencies"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+other_crate = { path = "other_crate" }
+
+[package.metadata.kani.unstable]
+stubbing = true

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

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

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected

@@ -0,0 +1,3 @@
+Autoharness: Checking function yes_harness against all possible inputs...
+Verification succeeded for - yes_harness
+Complete - 1 successfully verified functions, 0 failures, 1 total.

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z autoharness
+# We expect verification to fail, so the above command will produce an exit status of 1
+# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
+# So, exit with a status code of 0 explicitly.
+exit 0;

tests/script-based-pre/cargo_autoharness_dependencies/other_crate/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "other_crate"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tests/script-based-pre/cargo_autoharness_dependencies/other_crate/src/lib.rs

@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn no_harness(x: u8) -> u8 {
+    x + 1
+}

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

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This tests that the autoharness feature doesn't generate harnesses for functions outside the local crate.
+
+use other_crate;
+
+fn yes_harness(x: u8) -> u8 {
+    x
+}