Added --all-features flag. (rust-lang#1532)

* Added --all-features flag.

* Made the doc more detailed.

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,
+    /// Compiles Kani harnesses in all features of all packages selected on the command-line.
+    #[structopt(long)]
+    pub all_features: bool,
     /// Run Kani on all packages in the workspace.
     #[structopt(long)]
     pub workspace: bool,

kani-driver/src/call_cargo.rs

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

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

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

tests/cargo-kani/feature-flag/expected

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

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

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! 3 proof harnesses, 2 of them are feature-gated.
+
+#[kani::proof]
+fn check_proof() {
+    assert!(1 == 1);
+}
+
+#[cfg(feature = "A")]
+#[kani::proof]
+fn check_proof_a() {
+    assert!(2 == 2);
+}
+
+#[cfg(feature = "B")]
+#[kani::proof]
+fn check_proof_b() {
+    assert!(3 == 3);
+}