Add a test

model-checking · Jan 10, 2025 · cbab688 · cbab688
1 parent 9629796
commit cbab688
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 0 deletions.
diff --git a/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml b/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
@@ -0,0 +1,6 @@
+[package]
+name = "add"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
diff --git a/tests/script-based-pre/cargo_manifest_test/add/src/main.rs b/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
@@ -0,0 +1,4 @@
+#[kani::proof]
+fn main() {
+    1 + 1;
+}
diff --git a/tests/script-based-pre/cargo_manifest_test/config.yml b/tests/script-based-pre/cargo_manifest_test/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: manifest_test.sh
+expected: manifest_test.expected
diff --git a/tests/script-based-pre/cargo_manifest_test/manifest_test.expected b/tests/script-based-pre/cargo_manifest_test/manifest_test.expected
@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/script-based-pre/cargo_manifest_test/manifest_test.sh b/tests/script-based-pre/cargo_manifest_test/manifest_test.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test if Kani can correctly check if package in the workspace when
+# manifest-path presents.
+
+cargo kani --manifest-path=add/Cargo.toml --package add --debug
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Complete - 1 successfully verified harnesses, 0 failures, 1 total.