From b119b0e2e0a9f08e221e693eb9ee7b1c597ec3e7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 30 Aug 2023 16:45:27 -0700 Subject: [PATCH] Enable `-Z stubbing` and error out instead of ignore stub (#2678) Enable `-Z stubbing`, deprecate `--enable-stubbing`, and emit an error if the user tries to verify a harness that has stubs without explicitly enabling stubs. This used to be a warning before which was easy to miss. It was also hard to debug when the harness would take a while to run. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- kani-driver/src/args/mod.rs | 12 +++- kani-driver/src/call_single_file.rs | 2 +- kani-driver/src/harness_runner.rs | 61 +++++++++---------- .../stubbing-do-not-resolve/Cargo.toml | 4 +- .../harness/Cargo.toml | 5 +- .../stubbing-extern-path/Cargo.toml | 4 +- .../stubbing-foreign-method/Cargo.toml | 4 +- .../Cargo.toml | 4 +- .../Cargo.toml | 4 +- .../Cargo.toml | 4 +- .../stubbing-use-as-foreign/Cargo.toml | 4 +- .../stubbing-use-foreign/Cargo.toml | 4 +- .../stubbing-use-glob-foreign/Cargo.toml | 4 +- .../stubbing-use-in-foreign/Cargo.toml | 4 +- .../stubbing-validate-random/Cargo.toml | 4 +- .../stubbing-ws-packages/Cargo.toml | 5 +- .../Cargo.toml | 4 +- tests/cargo-ui/stubbing-flag/Cargo.toml | 3 +- .../expected/function-stubbing-error/expected | 2 + .../main.rs | 3 +- .../function-stubbing-warning/expected | 5 -- tests/kani/Stubbing/enum_method.rs | 2 +- tests/kani/Stubbing/fixme_issue_1953.rs | 2 +- tests/kani/Stubbing/foreign_functions.rs | 2 +- tests/kani/Stubbing/glob_cycle.rs | 2 +- tests/kani/Stubbing/glob_path.rs | 2 +- tests/kani/Stubbing/method_generic_type.rs | 2 +- tests/kani/Stubbing/multiple_harnesses.rs | 2 +- tests/kani/Stubbing/partial_harness_name.rs | 2 +- tests/kani/Stubbing/private_function.rs | 2 +- tests/kani/Stubbing/public_function.rs | 2 +- tests/kani/Stubbing/qualifiers.rs | 2 +- .../Stubbing/resolve_superseded_glob_use.rs | 2 +- tests/kani/Stubbing/resolve_use.rs | 2 +- tests/kani/Stubbing/resolve_use_as.rs | 2 +- tests/kani/Stubbing/resolve_use_glob.rs | 2 +- tests/kani/Stubbing/std_fs_read.rs | 2 +- tests/kani/Stubbing/struct_method.rs | 2 +- tests/kani/Stubbing/stub_harnesses.rs | 2 +- tests/kani/Stubbing/use_std_fs_read.rs | 2 +- .../Stubbing/validate_mismatched_traits.rs | 2 +- tests/ui/stub-attribute/attribute.rs | 2 +- .../deprecated-enable-stable/deprecated.rs | 16 +++++ .../deprecated-enable-stable/expected | 2 + 44 files changed, 115 insertions(+), 91 deletions(-) create mode 100644 tests/expected/function-stubbing-error/expected rename tests/expected/{function-stubbing-warning => function-stubbing-error}/main.rs (68%) delete mode 100644 tests/expected/function-stubbing-warning/expected create mode 100644 tests/ui/stubbing/deprecated-enable-stable/deprecated.rs create mode 100644 tests/ui/stubbing/deprecated-enable-stable/expected diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index bc927559ecb5..8be6bceab921 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -299,7 +299,7 @@ pub struct VerificationArgs { requires("enable_unstable"), conflicts_with("concrete_playback") )] - pub enable_stubbing: bool, + enable_stubbing: bool, /// Enable Kani coverage output alongside verification result #[arg(long, hide_short_help = true)] @@ -345,6 +345,12 @@ impl VerificationArgs { Some(Some(x)) => Some(x), // -j=x } } + + /// Is experimental stubbing enabled? + pub fn is_stubbing_enabled(&self) -> bool { + self.enable_stubbing + || self.common_args.unstable_features.contains(&UnstableFeatures::Stubbing) + } } #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)] @@ -617,6 +623,10 @@ impl ValidateArgs for VerificationArgs { } } + if self.enable_stubbing { + print_deprecated(&self.common_args, "--enable-stubbing", "-Z stubbing"); + } + if self.concrete_playback.is_some() && !self.common_args.unstable_features.contains(&UnstableFeatures::ConcretePlayback) { diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 1522071fdefd..30cdf88db835 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -92,7 +92,7 @@ impl KaniSession { flags.push("--write-json-symtab".into()); } - if self.args.enable_stubbing { + if self.args.is_stubbing_enabled() { flags.push("--enable-stubbing".into()); } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index fa1aef3d763a..2cd8bb7cbd70 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -4,14 +4,13 @@ use anyhow::{bail, Result}; use kani_metadata::{ArtifactType, HarnessMetadata}; use rayon::prelude::*; -use std::cmp::Ordering; use std::path::Path; use crate::args::OutputFormat; use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; use crate::session::KaniSession; -use crate::util::{error, warning}; +use crate::util::error; /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed. @@ -38,6 +37,8 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { &self, harnesses: &'pr [&HarnessMetadata], ) -> Result>> { + self.check_stubbing(harnesses)?; + let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses); let pool = { @@ -70,6 +71,33 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { Ok(results) } + + /// Return an error if the user is trying to verify a harness with stubs without enabling the + /// experimental feature. + fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> { + if !self.sess.args.is_stubbing_enabled() { + let with_stubs: Vec<_> = harnesses + .iter() + .filter_map(|harness| { + (!harness.attributes.stubs.is_empty()).then_some(harness.pretty_name.as_str()) + }) + .collect(); + match with_stubs.as_slice() { + [] => { /* do nothing */ } + [harness] => bail!( + "Use of unstable feature 'stubbing' in harness `{}`.\n\ + To enable stubbing, pass option `-Z stubbing`", + harness + ), + harnesses => bail!( + "Use of unstable feature 'stubbing' in harnesses `{}`.\n\ + To enable stubbing, pass option `-Z stubbing`", + harnesses.join("`, `") + ), + } + } + Ok(()) + } } impl KaniSession { @@ -108,33 +136,6 @@ impl KaniSession { } } - /// Prints a warning at the end of the verification if harness contained a stub but stubs were - /// not enabled. - fn stubbing_statuses(&self, results: &[HarnessResult]) { - if !self.args.enable_stubbing { - let ignored_stubs: Vec<_> = results - .iter() - .filter_map(|result| { - (!result.harness.attributes.stubs.is_empty()) - .then_some(result.harness.pretty_name.as_str()) - }) - .collect(); - match ignored_stubs.len().cmp(&1) { - Ordering::Equal => warning(&format!( - "harness `{}` contained stubs which were ignored.\n\ - To enable stubbing, pass options `--enable-unstable --enable-stubbing`", - ignored_stubs[0] - )), - Ordering::Greater => warning(&format!( - "harnesses `{}` contained stubs which were ignored.\n\ - To enable stubbing, pass options `--enable-unstable --enable-stubbing`", - ignored_stubs.join("`, `") - )), - Ordering::Less => {} - } - } - } - /// Concludes a session by printing a summary report and exiting the process with an /// error code (if applicable). /// @@ -195,8 +196,6 @@ impl KaniSession { } } - self.stubbing_statuses(results); - if failing > 0 { // Failure exit code without additional error message drop(self); diff --git a/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml b/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml index 85da4b7dc7e8..2b0e6273f0ae 100644 --- a/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml +++ b/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml @@ -11,5 +11,5 @@ edition = "2021" other_crate1 = { path = "other_crate1" } other_crate2 = { path = "other_crate2" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml b/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml index 4d26da916be8..cb4aedadd582 100644 --- a/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml +++ b/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml @@ -11,6 +11,7 @@ description = "Should test invoking double extern but found cycle issue" crate_b = { path = "../crate_b" } [package.metadata.kani.flags] -enable-unstable = true -enable-stubbing = true harness = ["check_inverted"] + +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-extern-path/Cargo.toml b/tests/cargo-kani/stubbing-extern-path/Cargo.toml index 58ee1c579e5f..5b9e08f1d8c0 100644 --- a/tests/cargo-kani/stubbing-extern-path/Cargo.toml +++ b/tests/cargo-kani/stubbing-extern-path/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-foreign-method/Cargo.toml b/tests/cargo-kani/stubbing-foreign-method/Cargo.toml index 3faa6d269800..54d2e3636d8e 100644 --- a/tests/cargo-kani/stubbing-foreign-method/Cargo.toml +++ b/tests/cargo-kani/stubbing-foreign-method/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml index 3faa6d269800..54d2e3636d8e 100644 --- a/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml +++ b/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml index 3faa6d269800..54d2e3636d8e 100644 --- a/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml +++ b/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml b/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml index 9a6a8e7cc903..b8fc26c97066 100644 --- a/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml +++ b/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml @@ -10,5 +10,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml index 6fb8f5632fac..d02d62cce077 100644 --- a/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml +++ b/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-use-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-foreign/Cargo.toml index 6c930116aeab..8eafd54bf89f 100644 --- a/tests/cargo-kani/stubbing-use-foreign/Cargo.toml +++ b/tests/cargo-kani/stubbing-use-foreign/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml index f6ea8cc1b0a4..cd59013a726e 100644 --- a/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml +++ b/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml index 4dcda9d3aa5d..ec2f3797ee4d 100644 --- a/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml +++ b/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] other_crate = { path = "other_crate" } -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-validate-random/Cargo.toml b/tests/cargo-kani/stubbing-validate-random/Cargo.toml index 099cc3d4d5b9..ef03456dd1aa 100644 --- a/tests/cargo-kani/stubbing-validate-random/Cargo.toml +++ b/tests/cargo-kani/stubbing-validate-random/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] rand = "0.8.5" -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-kani/stubbing-ws-packages/Cargo.toml b/tests/cargo-kani/stubbing-ws-packages/Cargo.toml index 2ff3f16833d4..a2169dbc134e 100644 --- a/tests/cargo-kani/stubbing-ws-packages/Cargo.toml +++ b/tests/cargo-kani/stubbing-ws-packages/Cargo.toml @@ -5,6 +5,5 @@ [workspace] members = ["dependency", "top"] -[workspace.metadata.kani.flags] -enable-unstable=true -enable-stubbing=true +[workspace.metadata.kani.unstable] +stubbing=true diff --git a/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml b/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml index 7562cf1eb7a3..8e8095e249e7 100644 --- a/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml +++ b/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml @@ -7,5 +7,5 @@ edition = "2021" [dependencies] -[package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true } \ No newline at end of file +[package.metadata.kani.unstable] +stubbing = true diff --git a/tests/cargo-ui/stubbing-flag/Cargo.toml b/tests/cargo-ui/stubbing-flag/Cargo.toml index f94fba420728..66541c9f3ba5 100644 --- a/tests/cargo-ui/stubbing-flag/Cargo.toml +++ b/tests/cargo-ui/stubbing-flag/Cargo.toml @@ -8,4 +8,5 @@ edition = "2021" [dependencies] [package.metadata.kani] -flags = { enable-unstable=true, enable-stubbing=true, harness="main" } +flags = { harness="main" } +unstable = { stubbing=true } diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected new file mode 100644 index 000000000000..6adf1ad27631 --- /dev/null +++ b/tests/expected/function-stubbing-error/expected @@ -0,0 +1,2 @@ +error: Use of unstable feature 'stubbing' in harness `main`. +To enable stubbing, pass option `-Z stubbing` diff --git a/tests/expected/function-stubbing-warning/main.rs b/tests/expected/function-stubbing-error/main.rs similarity index 68% rename from tests/expected/function-stubbing-warning/main.rs rename to tests/expected/function-stubbing-error/main.rs index 4305f4d398be..4b206bfaee44 100644 --- a/tests/expected/function-stubbing-warning/main.rs +++ b/tests/expected/function-stubbing-error/main.rs @@ -3,8 +3,7 @@ // // kani-flags: --harness main // -//! This tests whether we issue a warning if a stub is specified for a harness -//! but stubbing is not enabled. +//! This tests whether we abort if a stub is specified for a harness but stubbing is not enabled. fn foo() -> u32 { 0 diff --git a/tests/expected/function-stubbing-warning/expected b/tests/expected/function-stubbing-warning/expected deleted file mode 100644 index 5a5f9f608542..000000000000 --- a/tests/expected/function-stubbing-warning/expected +++ /dev/null @@ -1,5 +0,0 @@ -Checking harness main... -Failed Checks: assertion failed: foo() == 42 - -warning: harness `main` contained stubs which were ignored.\ -To enable stubbing, pass options `--enable-unstable --enable-stubbing` diff --git a/tests/kani/Stubbing/enum_method.rs b/tests/kani/Stubbing/enum_method.rs index a5cf43d214a0..ac1c5351b976 100644 --- a/tests/kani/Stubbing/enum_method.rs +++ b/tests/kani/Stubbing/enum_method.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests stubbing for methods in local enums. diff --git a/tests/kani/Stubbing/fixme_issue_1953.rs b/tests/kani/Stubbing/fixme_issue_1953.rs index 1f319a0a0e91..55df2d4dc835 100644 --- a/tests/kani/Stubbing/fixme_issue_1953.rs +++ b/tests/kani/Stubbing/fixme_issue_1953.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --enable-stubbing --harness main +// kani-flags: -Z stubbing --harness main // // We currently require a stub and the original/function method to have the same // names for generic parameters; instead, we should allow for renaming. diff --git a/tests/kani/Stubbing/foreign_functions.rs b/tests/kani/Stubbing/foreign_functions.rs index 8c2ff0812905..07306b1cdf6b 100644 --- a/tests/kani/Stubbing/foreign_functions.rs +++ b/tests/kani/Stubbing/foreign_functions.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --enable-stubbing +// kani-flags: -Z stubbing // //! Check support for stubbing out foreign functions. diff --git a/tests/kani/Stubbing/glob_cycle.rs b/tests/kani/Stubbing/glob_cycle.rs index 42600809c7bf..54aa066f1622 100644 --- a/tests/kani/Stubbing/glob_cycle.rs +++ b/tests/kani/Stubbing/glob_cycle.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness check_stub --enable-unstable --enable-stubbing +// kani-flags: --harness check_stub -Z stubbing //! Test that stub can solve glob cycles. pub mod mod_a { diff --git a/tests/kani/Stubbing/glob_path.rs b/tests/kani/Stubbing/glob_path.rs index 17a9e7ed4264..72ec8a07d980 100644 --- a/tests/kani/Stubbing/glob_path.rs +++ b/tests/kani/Stubbing/glob_path.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness check_stub --enable-unstable --enable-stubbing +// kani-flags: --harness check_stub -Z stubbing //! Test that stub can solve glob cycles even when the path expands the cycle. pub mod mod_a { diff --git a/tests/kani/Stubbing/method_generic_type.rs b/tests/kani/Stubbing/method_generic_type.rs index 55bad2c72715..804c2c5c7f5e 100644 --- a/tests/kani/Stubbing/method_generic_type.rs +++ b/tests/kani/Stubbing/method_generic_type.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests stubbing for methods of a local type that has generic parameters. diff --git a/tests/kani/Stubbing/multiple_harnesses.rs b/tests/kani/Stubbing/multiple_harnesses.rs index 59d4199b601f..ac20b53e515e 100644 --- a/tests/kani/Stubbing/multiple_harnesses.rs +++ b/tests/kani/Stubbing/multiple_harnesses.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --enable-stubbing +// kani-flags: -Z stubbing //! Check that Kani can handle a different combination of stubs in //! the same crate. diff --git a/tests/kani/Stubbing/partial_harness_name.rs b/tests/kani/Stubbing/partial_harness_name.rs index c08de8c226d9..eae475154d1d 100644 --- a/tests/kani/Stubbing/partial_harness_name.rs +++ b/tests/kani/Stubbing/partial_harness_name.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness mod2::harness --enable-unstable --enable-stubbing +// kani-flags: --harness mod2::harness -Z stubbing // //! This tests whether we correctly find harnesses during stubbing that are //! specified with a partially qualified name. diff --git a/tests/kani/Stubbing/private_function.rs b/tests/kani/Stubbing/private_function.rs index d112731444c7..818c94c51623 100644 --- a/tests/kani/Stubbing/private_function.rs +++ b/tests/kani/Stubbing/private_function.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests stubbing for private local functions. diff --git a/tests/kani/Stubbing/public_function.rs b/tests/kani/Stubbing/public_function.rs index 85a25e7d48e8..8257081241b5 100644 --- a/tests/kani/Stubbing/public_function.rs +++ b/tests/kani/Stubbing/public_function.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests stubbing for public local functions. diff --git a/tests/kani/Stubbing/qualifiers.rs b/tests/kani/Stubbing/qualifiers.rs index b9b4aac560a0..06cee979883b 100644 --- a/tests/kani/Stubbing/qualifiers.rs +++ b/tests/kani/Stubbing/qualifiers.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests resolving stubs with the path qualifiers `self`, `super`, and //! `crate`. diff --git a/tests/kani/Stubbing/resolve_superseded_glob_use.rs b/tests/kani/Stubbing/resolve_superseded_glob_use.rs index 83f1b3527a0c..e639437133f4 100644 --- a/tests/kani/Stubbing/resolve_superseded_glob_use.rs +++ b/tests/kani/Stubbing/resolve_superseded_glob_use.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! Tests to make sure that, when we are resolving paths in `kani::stub` //! attributes, we prioritize those that do not come from glob imports. diff --git a/tests/kani/Stubbing/resolve_use.rs b/tests/kani/Stubbing/resolve_use.rs index 9bd25bc90bb5..ac1f6f7325f8 100644 --- a/tests/kani/Stubbing/resolve_use.rs +++ b/tests/kani/Stubbing/resolve_use.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing +// kani-flags: --harness my_mod::harness -Z stubbing // //! This tests whether we take into account simple local uses (`use XXX;`) when //! resolving paths in `kani::stub` attributes. diff --git a/tests/kani/Stubbing/resolve_use_as.rs b/tests/kani/Stubbing/resolve_use_as.rs index b661636fae7e..790e26e575e9 100644 --- a/tests/kani/Stubbing/resolve_use_as.rs +++ b/tests/kani/Stubbing/resolve_use_as.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing +// kani-flags: --harness my_mod::harness -Z stubbing // //! This tests whether we take into account simple local use-as statements (`use //! XXX as YYY;`) when resolving paths in `kani::stub` attributes. diff --git a/tests/kani/Stubbing/resolve_use_glob.rs b/tests/kani/Stubbing/resolve_use_glob.rs index f9092e9f1a55..a5e85ce7e10c 100644 --- a/tests/kani/Stubbing/resolve_use_glob.rs +++ b/tests/kani/Stubbing/resolve_use_glob.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing +// kani-flags: --harness my_mod::harness -Z stubbing // //! This tests whether we take into account local use-glob statements (`use //! XXX::*;`) when resolving paths in `kani::stub` attributes. diff --git a/tests/kani/Stubbing/std_fs_read.rs b/tests/kani/Stubbing/std_fs_read.rs index 397487a3a5b4..fa9d55c06813 100644 --- a/tests/kani/Stubbing/std_fs_read.rs +++ b/tests/kani/Stubbing/std_fs_read.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests stubbing `std` functions like `std::fs::read`. diff --git a/tests/kani/Stubbing/struct_method.rs b/tests/kani/Stubbing/struct_method.rs index b939bf7b417a..0270941ef705 100644 --- a/tests/kani/Stubbing/struct_method.rs +++ b/tests/kani/Stubbing/struct_method.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests stubbing for methods in local structs. diff --git a/tests/kani/Stubbing/stub_harnesses.rs b/tests/kani/Stubbing/stub_harnesses.rs index f83dc309277e..b7969f74d03d 100644 --- a/tests/kani/Stubbing/stub_harnesses.rs +++ b/tests/kani/Stubbing/stub_harnesses.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness check --enable-unstable --enable-stubbing +// kani-flags: --harness check -Z stubbing // //! This tests whether we provide a user friendly error if more than one harness has stubs diff --git a/tests/kani/Stubbing/use_std_fs_read.rs b/tests/kani/Stubbing/use_std_fs_read.rs index e174e49e93a9..8beee26bbbf3 100644 --- a/tests/kani/Stubbing/use_std_fs_read.rs +++ b/tests/kani/Stubbing/use_std_fs_read.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests whether we can correctly account for `use` statements with `std` //! functions like `std::fs::read` when resolving paths in `kani::stub` diff --git a/tests/kani/Stubbing/validate_mismatched_traits.rs b/tests/kani/Stubbing/validate_mismatched_traits.rs index 32d49593bc18..f575e2bb6fa3 100644 --- a/tests/kani/Stubbing/validate_mismatched_traits.rs +++ b/tests/kani/Stubbing/validate_mismatched_traits.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests that we allow trait mismatches between the stub and the original //! function/method so long as they do not lead to a trait method call being diff --git a/tests/ui/stub-attribute/attribute.rs b/tests/ui/stub-attribute/attribute.rs index 2e3b81fb09ea..19fdf5b5b05b 100644 --- a/tests/ui/stub-attribute/attribute.rs +++ b/tests/ui/stub-attribute/attribute.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// +// kani-flags: -Z stubbing //! Checks that the `kani::stub` attribute is accepted fn foo() {} diff --git a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs new file mode 100644 index 000000000000..a5686af20a35 --- /dev/null +++ b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-unstable --enable-stubbing +//! Checks that the `kani::stub` attribute is accepted + +fn foo() { + unreachable!(); +} + +fn bar() {} + +#[kani::proof] +#[kani::stub(foo, bar)] +fn main() { + foo(); +} diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected new file mode 100644 index 000000000000..eb05b8cf9812 --- /dev/null +++ b/tests/ui/stubbing/deprecated-enable-stable/expected @@ -0,0 +1,2 @@ +warning: The `--enable-stubbing` option is deprecated. This option will be removed soon. Consider using `-Z stubbing` instead +VERIFICATION:- SUCCESSFUL