Add --workspace to cargo kani. (rust-lang#1530)

* Added workspace flag and tests.

* Added license, adjusted comments.

* Fixed docs.

Author: Yoshiki Takashima

kani-driver/src/args.rs

@@ -114,6 +114,9 @@ pub struct KaniArgs {
     /// Kani will only compile the crate. No verification will be performed
     #[structopt(long, hidden_short_help(true))]
     pub only_codegen: bool,
+    /// Run Kani on all packages in the workspace.
+    #[structopt(long)]
+    pub workspace: bool,
 
     /// Specify the value used for loop unwinding in CBMC
     #[structopt(long)]

kani-driver/src/call_cargo.rs

@@ -52,6 +52,10 @@ impl KaniSession {
             args.push("build".into());
         }
 
+        if self.args.workspace {
+            args.push("--workspace".into());
+        }
+
         args.push("--target".into());
         args.push(build_target.into());
 

tests/cargo-kani/ws-flag/Cargo.toml

@@ -0,0 +1,20 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "ws-flag"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[workspace]
+members = [
+  "libcrate",
+]
+
+
+[dependencies]
+
+[package.metadata.kani.flags]
+workspace = true

tests/cargo-kani/ws-flag/expected

@@ -0,0 +1 @@
+2 successfully verified harnesses

tests/cargo-kani/ws-flag/libcrate/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "libcrate"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-kani/ws-flag/libcrate/src/lib.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! test in sub-crate.
+
+#[kani::proof]
+fn check_libcrate_proof() {
+    assert!(1 == 1);
+}

tests/cargo-kani/ws-flag/src/lib.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! test in top crate.
+
+#[kani::proof]
+fn check_toplevel_proof() {
+    assert!(1 == 1);
+}