From f1ae1d9d924f8ea8f6a5c1557cd75ef27deb3108 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 2 Jul 2024 22:00:34 -0700 Subject: [PATCH] Deprecate `--enable-unstable` and `--restrict-vtable` For unstable options, require `-Z unstable-options` instead. `--restrict-vtable` is deprecated in favor of `-Z restrict-vtable` --- kani-compiler/src/kani_middle/mod.rs | 2 +- kani-driver/src/args/common.rs | 26 ++- kani-driver/src/args/mod.rs | 177 ++++++++++++------ kani-driver/src/assess/mod.rs | 2 +- kani-driver/src/assess/scan.rs | 3 +- kani-driver/src/cbmc_property_renderer.rs | 2 +- kani_metadata/src/unstable.rs | 2 + scripts/assess-scan-regression.sh | 2 +- scripts/exps/assess-scan-on-repos.sh | 2 +- ...doesnt_call_crate_with_global_asm.expected | 2 +- tests/cargo-kani/assess-artifacts/Cargo.toml | 3 +- .../assess-workspace-artifacts/Cargo.toml | 3 +- .../cargo-kani/simple-config-toml/Cargo.toml | 6 +- tests/cargo-kani/simple-kissat/Cargo.toml | 4 +- tests/cargo-ui/assess-error/Cargo.toml | 3 +- .../function-contract/history/stub.rs | 2 +- .../whole-struct/refcell.rs | 2 +- .../expected/loop-contract/multiple_loops.rs | 2 +- .../expected/loop-contract/small_slice_eq.rs | 2 +- .../object-bits/insufficient/expected | 2 +- .../expected/object-bits/insufficient/main.rs | 2 +- tests/expected/unwind-flags-conflict/main.rs | 2 +- .../virtio-balloon-compact/ignore-main.rs | 2 +- tests/kani/DynTrait/any_cast_int.rs | 2 +- tests/kani/DynTrait/vtable_restrictions.rs | 2 +- tests/kani/Overflow/pointer_overflow_fail.rs | 2 +- tests/ui/concrete-playback/array/main.rs | 2 +- tests/ui/concrete-playback/bool/main.rs | 2 +- tests/ui/concrete-playback/cover/main.rs | 2 +- tests/ui/concrete-playback/custom/main.rs | 2 +- tests/ui/concrete-playback/f32/main.rs | 2 +- tests/ui/concrete-playback/f64/main.rs | 2 +- tests/ui/concrete-playback/i128/main.rs | 2 +- tests/ui/concrete-playback/i16/main.rs | 2 +- tests/ui/concrete-playback/i32/main.rs | 2 +- tests/ui/concrete-playback/i64/main.rs | 2 +- tests/ui/concrete-playback/i8/main.rs | 2 +- tests/ui/concrete-playback/isize/main.rs | 2 +- .../concrete-playback/mult-harnesses/main.rs | 2 +- tests/ui/concrete-playback/non_zero/main.rs | 2 +- tests/ui/concrete-playback/option/main.rs | 2 +- tests/ui/concrete-playback/result/main.rs | 2 +- .../concrete-playback/slice-formula/main.rs | 2 +- tests/ui/concrete-playback/u128/main.rs | 2 +- tests/ui/concrete-playback/u16/main.rs | 2 +- tests/ui/concrete-playback/u32/main.rs | 2 +- tests/ui/concrete-playback/u64/main.rs | 2 +- tests/ui/concrete-playback/u8/main.rs | 2 +- .../ui/concrete-playback/unsupported/loop.rs | 2 +- tests/ui/concrete-playback/usize/main.rs | 2 +- tests/ui/invalid-cbmc-function-arg/main.rs | 2 +- .../main_signed/main_signed.rs | 2 +- .../main_unsigned/main_unsigned.rs | 2 +- tools/compiletest/src/runtest.rs | 2 +- 54 files changed, 209 insertions(+), 108 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index dbdd421fcc36..508e92f76479 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -44,7 +44,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { if !ignore_asm { let error_msg = format!( "Crate {krate} contains global ASM, which is not supported by Kani. Rerun with \ - `--enable-unstable --ignore-global-asm` to suppress this error \ + `-Z unstable-options --ignore-global-asm` to suppress this error \ (**Verification results may be impacted**).", ); tcx.dcx().err(error_msg); diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index 3333ee67badf..9f845b79f41e 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define arguments that should be common to all subcommands in Kani. -use crate::args::ValidateArgs; +use crate::args::{ValidateArgs, print_deprecated}; use clap::{error::Error, error::ErrorKind}; pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature}; @@ -43,6 +43,30 @@ impl ValidateArgs for CommonArgs { } } +impl CommonArgs { + pub fn check_unstable( + &self, + enabled: bool, + argument: &str, + required: UnstableFeature, + ) -> Result<(), Error> { + if enabled && !self.unstable_features.contains(required) { + let z_feature = format!("-Z {required}"); + if self.enable_unstable { + print_deprecated(self, "--enable-unstable", &z_feature); + } else { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `{argument}` argument is unstable and requires `{z_feature}` to be used.", + ), + )); + } + } + Ok(()) + } +} + /// The verbosity level to be used in Kani. pub trait Verbosity { /// Whether we should be quiet. diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 0038020d58dd..9ba06826d200 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -181,7 +181,7 @@ pub enum CargoKaniSubcommand { pub struct VerificationArgs { /// Temporary option to trigger assess mode for out test suite /// where we are able to add options but not subcommands - #[arg(long, hide = true, requires("enable_unstable"))] + #[arg(long, hide = true)] pub assess: bool, /// Generate concrete playback unit test. @@ -195,9 +195,9 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub keep_temps: bool, - /// Generate C file equivalent to inputted program. - /// This feature is unstable and it requires `--enable-unstable` to be used - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + /// Generate C file equivalent to inputted program for debug purpose. + /// This feature is unstable, and it requires `-Z unstable-options` to be used + #[arg(long, hide_short_help = true)] pub gen_c: bool, /// Directory for all generated artifacts. @@ -247,11 +247,10 @@ pub struct VerificationArgs { #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))] pub solver: Option, /// Pass through directly to CBMC; must be the last flag. - /// This feature is unstable and it requires `--enable_unstable` to be used + /// This feature is unstable and it requires `-Z unstable-options` to be used #[arg( long, allow_hyphen_values = true, - requires("enable_unstable"), num_args(0..) )] // consumes everything @@ -261,19 +260,19 @@ pub struct VerificationArgs { /// Omit the flag entirely to run sequentially (i.e. one thread). /// Pass -j to run with the thread pool's default number of threads. /// Pass -j to specify N threads. - #[arg(short, long, hide_short_help = true, requires("enable_unstable"))] + #[arg(short, long, hide_short_help = true)] pub jobs: Option>, /// Enable extra pointer checks such as invalid pointers in relation operations and pointer /// arithmetic overflow. /// This feature is unstable and it may yield false counter examples. It requires - /// `--enable-unstable` to be used - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + /// `-Z unstable-options` to be used + #[arg(long, hide_short_help = true)] pub extra_pointer_checks: bool, /// Restrict the targets of virtual table function pointer calls. - /// This feature is unstable and it requires `--enable-unstable` to be used - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + /// This feature is unstable and it requires `-Z restrict-vtable` to be used + #[arg(long, hide_short_help = true, conflicts_with = "no_restrict_vtable")] pub restrict_vtable: bool, /// Disable restricting the targets of virtual table function pointer calls #[arg(long, hide_short_help = true)] @@ -284,7 +283,7 @@ pub struct VerificationArgs { /// Do not error out for crates containing `global_asm!`. /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + #[arg(long, hide_short_help = true)] pub ignore_global_asm: bool, /// Write the GotoC symbol table to a file in JSON format instead of goto binary format. @@ -292,18 +291,17 @@ pub struct VerificationArgs { pub write_json_symtab: bool, /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct. - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + #[arg(long, hide_short_help = true)] pub run_sanity_checks: bool, /// Disable CBMC's slice formula which prevents values from being assigned to redundant variables in traces. - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + #[arg(long, hide_short_help = true)] pub no_slice_formula: bool, /// Synthesize loop contracts for all loops. #[arg( long, hide_short_help = true, - requires("enable_unstable"), conflicts_with("unwind"), conflicts_with("default_unwind") )] @@ -351,6 +349,8 @@ pub struct VerificationArgs { impl VerificationArgs { pub fn restrict_vtable(&self) -> bool { self.restrict_vtable + || (self.common_args.unstable_features.contains(UnstableFeature::RestrictVtable) + && !self.no_restrict_vtable) // if we flip the default, this will become: !self.no_restrict_vtable } @@ -538,16 +538,14 @@ impl ValidateArgs for CargoKaniArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; self.command.validate()?; - // --assess requires --enable-unstable, but the subcommand needs manual checking - if (matches!(self.command, Some(CargoKaniSubcommand::Assess(_))) || self.verify_opts.assess) - && !self.verify_opts.common_args.enable_unstable - { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "Assess is unstable and requires 'cargo kani --enable-unstable assess'", - )); - } - Ok(()) + + // --assess requires -Z unstable-options, but the subcommand needs manual checking + self.verify_opts.common_args.check_unstable( + (matches!(self.command, Some(CargoKaniSubcommand::Assess(_))) + || self.verify_opts.assess), + "assess", + UnstableFeature::UnstableOptions, + ) } } @@ -630,20 +628,78 @@ impl ValidateArgs for VerificationArgs { } } - if self.concrete_playback.is_some() - && !self.common_args.unstable_features.contains(UnstableFeature::ConcretePlayback) - { - if self.common_args.enable_unstable { - print_deprecated(&self.common_args, "--enable-unstable", "-Z concrete-playback"); - } else { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `--concrete-playback` argument is unstable and requires `-Z \ - concrete-playback` to be used.", - )); - } + self.common_args.check_unstable( + self.concrete_playback.is_some(), + "--concrete-playback", + UnstableFeature::ConcretePlayback, + )?; + + self.common_args.check_unstable( + !self.c_lib.is_empty(), + "--c-lib", + UnstableFeature::CFfi, + )?; + + self.common_args.check_unstable(self.gen_c, "--gen-c", UnstableFeature::UnstableOptions)?; + + self.common_args.check_unstable( + !self.cbmc_args.is_empty(), + "--cbmc-args", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.jobs.is_some(), + "--jobs", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.extra_pointer_checks, + "--extra-pointer-checks", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.ignore_global_asm, + "--ignore-global-asm", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.run_sanity_checks, + "--run-sanity-checks", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.no_slice_formula, + "--no-slice-formula", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.synthesize_loop_contracts, + "--synthesize-loop-contracts", + UnstableFeature::UnstableOptions, + )?; + + if self.restrict_vtable { + // Deprecated `--restrict-vtable` in favor our `-Z restrict-vtable`. + print_deprecated(&self.common_args, "--restrict-vtable", "-Z restrict-vtable"); + self.common_args.check_unstable( + true, + "--restrict-vtable", + UnstableFeature::RestrictVtable, + )?; } + self.common_args.check_unstable( + self.no_restrict_vtable, + "--no-restrict-vtable", + UnstableFeature::RestrictVtable, + )?; + if !self.c_lib.is_empty() && !self.common_args.unstable_features.contains(UnstableFeature::CFfi) { @@ -787,7 +843,7 @@ mod tests { let a = StandaloneArgs::try_parse_from(vec![ "kani", "file.rs", - "--enable-unstable", + "-Zunstable-options", "--cbmc-args", "--multiple", "args", @@ -798,7 +854,7 @@ mod tests { let _b = StandaloneArgs::try_parse_from(vec![ "kani", "file.rs", - "--enable-unstable", + "-Zunstable-options", "--cbmc-args", ]) .unwrap(); @@ -840,13 +896,13 @@ mod tests { assert!(b.is_ok()); } - fn check(args: &str, require_unstable: bool, pred: fn(StandaloneArgs) -> bool) { + fn check(args: &str, feature: Option, pred: fn(StandaloneArgs) -> bool) { let mut res = parse_unstable_disabled(&args); - if require_unstable { - // Should fail without --enable-unstable. + if let Some(unstable) = feature { + // Should fail without -Z unstable-options. assert_eq!(res.unwrap_err().kind(), ErrorKind::MissingRequiredArgument); - // Should succeed with --enable-unstable. - res = parse_unstable_enabled(&args); + // Should succeed with -Z unstable-options. + res = parse_unstable_enabled(&args, unstable); } assert!(res.is_ok()); assert!(pred(res.unwrap())); @@ -854,7 +910,7 @@ mod tests { macro_rules! check_unstable_flag { ($args:expr, $name:ident) => { - check($args, true, |p| p.verify_opts.$name) + check($args, Some(UnstableFeature::UnstableOptions), |p| p.verify_opts.$name) }; } @@ -891,22 +947,35 @@ mod tests { fn parse_unstable_disabled(args: &str) -> Result { let args = format!("kani file.rs {args}"); - StandaloneArgs::try_parse_from(args.split(' ')) + let parse_res = StandaloneArgs::try_parse_from(args.split(' '))?; + parse_res.verify_opts.validate()?; + Ok(parse_res) } - fn parse_unstable_enabled(args: &str) -> Result { - let args = format!("kani --enable-unstable file.rs {args}"); - StandaloneArgs::try_parse_from(args.split(' ')) + fn parse_unstable_enabled( + args: &str, + unstable: UnstableFeature, + ) -> Result { + let args = format!("kani -Z {} file.rs {args}", unstable); + let parse_res = StandaloneArgs::try_parse_from(args.split(' '))?; + parse_res.verify_opts.validate()?; + Ok(parse_res) } #[test] fn check_restrict_vtable_unstable() { - check_unstable_flag!("--restrict-vtable", restrict_vtable); + let restrict_vtable = |args: StandaloneArgs| args.verify_opts.restrict_vtable(); + check("--restrict-vtable", Some(UnstableFeature::RestrictVtable), restrict_vtable); } #[test] fn check_restrict_cbmc_args() { - check_opt!("--cbmc-args --json-ui", true, cbmc_args, vec!["--json-ui"]); + check_opt!( + "--cbmc-args --json-ui", + Some(UnstableFeature::UnstableOptions), + cbmc_args, + vec!["--json-ui"] + ); } #[test] @@ -938,11 +1007,11 @@ mod tests { #[test] fn check_concrete_playback_conflicts() { expect_validation_error( - "kani --concrete-playback=print --quiet --enable-unstable test.rs", + "kani --concrete-playback=print --quiet -Z concrete-playback test.rs", ErrorKind::ArgumentConflict, ); expect_validation_error( - "kani --concrete-playback=inplace --output-format=old --enable-unstable test.rs", + "kani --concrete-playback=inplace --output-format=old -Z concrete-playback test.rs", ErrorKind::ArgumentConflict, ); } @@ -1010,7 +1079,7 @@ mod tests { #[test] fn check_cbmc_args_lean_backend() { - let args = "kani input.rs -Z lean --enable-unstable --cbmc-args --object-bits 10" + let args = "kani input.rs -Z lean -Z unstable-options --cbmc-args --object-bits 10" .split_whitespace(); let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); assert_eq!(err.kind(), ErrorKind::ArgumentConflict); diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index 4ee82e48389c..ec91918ac8b5 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -49,7 +49,7 @@ fn assess_project(mut session: KaniSession) -> Result { session.codegen_tests = true; if session.args.jobs.is_none() { // assess will default to fully parallel instead of single-threaded. - // can be overridden with e.g. `cargo kani --enable-unstable -j 8 assess` + // can be overridden with e.g. `cargo kani -Z unstable-options -j 8 assess` session.args.jobs = Some(None); // -j, num_cpu } diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 7ce29bb64b33..63a778b294b4 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -179,7 +179,8 @@ fn invoke_assess( // TODO: -p likewise, probably fixed with a "CargoArgs" refactoring // Additionally, this should be `--manifest-path` but `cargo kani` doesn't support that yet. cmd.arg("-p").arg(package); - cmd.arg("--enable-unstable"); // This has to be after `-p` due to an argument parsing bug in kani-driver + // This has to be after `-p` due to an argument parsing bug in kani-driver + cmd.arg("-Zunstable-options"); cmd.args(["assess", "--emit-metadata"]) .arg(outfile) .current_dir(dir) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 78ee9dd8ea02..cc48449e01b2 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -456,7 +456,7 @@ fn postprocess_error_message(message: ParserItem) -> ParserItem { { ParserItem::Message { message_text: message_text - .replace("--object-bits ", "--enable-unstable --cbmc-args --object-bits "), + .replace("--object-bits ", "-Z unstable-options --cbmc-args --object-bits "), message_type: String::from("ERROR"), } } else { diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index e4f5bcaadd57..cb7aff27fc68 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -102,6 +102,8 @@ pub enum UnstableFeature { List, /// Kani APIs related to floating-point operations (e.g. `float_to_int_in_range`) FloatLib, + /// Enable vtable restriction. + RestrictVtable, } impl UnstableFeature { diff --git a/scripts/assess-scan-regression.sh b/scripts/assess-scan-regression.sh index f349219d5389..23800bb632f6 100755 --- a/scripts/assess-scan-regression.sh +++ b/scripts/assess-scan-regression.sh @@ -10,7 +10,7 @@ KANI_DIR=$SCRIPT_DIR/.. echo "Running assess scan test:" cd $KANI_DIR/tests/assess-scan-test-scaffold -cargo kani --enable-unstable assess scan +cargo kani -Z unstable-options assess scan # Clean up (cd foo && cargo clean) diff --git a/scripts/exps/assess-scan-on-repos.sh b/scripts/exps/assess-scan-on-repos.sh index bb863a85920c..eaa6acb65f35 100755 --- a/scripts/exps/assess-scan-on-repos.sh +++ b/scripts/exps/assess-scan-on-repos.sh @@ -61,7 +61,7 @@ popd echo "Starting assess scan..." -time cargo kani --only-codegen --enable-unstable assess scan \ +time cargo kani --only-codegen -Z unstable-options assess scan \ --filter-packages-file $NAME_FILE \ --emit-metadata ./scan-results.json diff --git a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected index 961b5f960b0b..9ccdc7eff3f5 100644 --- a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected +++ b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected @@ -1 +1 @@ -error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**). +error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `-Z unstable-options --ignore-global-asm` to suppress this error (**Verification results may be impacted**). diff --git a/tests/cargo-kani/assess-artifacts/Cargo.toml b/tests/cargo-kani/assess-artifacts/Cargo.toml index 050744568ae5..7b40e3443500 100644 --- a/tests/cargo-kani/assess-artifacts/Cargo.toml +++ b/tests/cargo-kani/assess-artifacts/Cargo.toml @@ -9,4 +9,5 @@ edition = "2021" # See src/lib.rs for a comment on this tests's purpose [package.metadata.kani] -flags = { assess=true, enable-unstable=true } +flags = { assess = true } +unstable = { unstable-options = true } diff --git a/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml b/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml index 17edf5074901..1e041ae4734d 100644 --- a/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml +++ b/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml @@ -9,7 +9,8 @@ edition = "2021" # See src/lib.rs for a comment on this tests's purpose [package.metadata.kani] -flags = { assess=true, enable-unstable=true, workspace=true } +flags = { assess = true, workspace = true } +unstable = { unstable-options = true } [workspace] members = ["subpackage"] diff --git a/tests/cargo-kani/simple-config-toml/Cargo.toml b/tests/cargo-kani/simple-config-toml/Cargo.toml index 09e79382683a..d8b0ad81b436 100644 --- a/tests/cargo-kani/simple-config-toml/Cargo.toml +++ b/tests/cargo-kani/simple-config-toml/Cargo.toml @@ -9,6 +9,6 @@ edition = "2018" [workspace] -[kani.flags] -enable-unstable = true -gen-c = true +[package.metadata.kani] +flags = { gen-c = true } +unstable = { unstable-options = true } diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml index 3bde94c619fb..46d329b8a498 100644 --- a/tests/cargo-kani/simple-kissat/Cargo.toml +++ b/tests/cargo-kani/simple-kissat/Cargo.toml @@ -11,5 +11,7 @@ description = "Tests that Kani can be invoked with Kissat" [dependencies] [kani.flags] -enable-unstable = true cbmc-args = ["--external-sat-solver", "kissat" ] + +[package.metadata.kani] +unstable = { unstable-options = true } diff --git a/tests/cargo-ui/assess-error/Cargo.toml b/tests/cargo-ui/assess-error/Cargo.toml index e82e43e9ccca..9480d8519d57 100644 --- a/tests/cargo-ui/assess-error/Cargo.toml +++ b/tests/cargo-ui/assess-error/Cargo.toml @@ -9,4 +9,5 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [package.metadata.kani] -flags = { assess=true, enable-unstable=true } +flags = { assess = true } +unstable = { unstable-options = true } diff --git a/tests/expected/function-contract/history/stub.rs b/tests/expected/function-contract/history/stub.rs index ce795bea6990..5ede5fed16ee 100644 --- a/tests/expected/function-contract/history/stub.rs +++ b/tests/expected/function-contract/history/stub.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // This test consumes > 9 GB of memory with 16 object bits. Reducing the number // of object bits to 8 to avoid running out of memory. -// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 8 +// kani-flags: -Zfunction-contracts -Z unstable-options --cbmc-args --object-bits 8 #[kani::ensures(|result| old(*ptr + *ptr) == *ptr)] #[kani::requires(*ptr < 100)] diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs index 518c8140ea37..d7022b04c823 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Temporarily reduce the number of object bits till // https://github.com/model-checking/kani/issues/3611 is fixed -// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12 +// kani-flags: -Zfunction-contracts -Z unstable-options --cbmc-args --object-bits 12 /// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct use std::cell::RefCell; diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs index b99278d32b43..58edf276a949 100644 --- a/tests/expected/loop-contract/multiple_loops.rs +++ b/tests/expected/loop-contract/multiple_loops.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --object-bits 8 +// kani-flags: -Z loop-contracts -Z unstable-options --cbmc-args --object-bits 8 //! Check if loop contracts is correctly applied. diff --git a/tests/expected/loop-contract/small_slice_eq.rs b/tests/expected/loop-contract/small_slice_eq.rs index 4c97d8a18502..2fd41accc07e 100644 --- a/tests/expected/loop-contract/small_slice_eq.rs +++ b/tests/expected/loop-contract/small_slice_eq.rs @@ -6,7 +6,7 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// kani-flags: -Z loop-contracts -Z mem-predicates --enable-unstable --cbmc-args --object-bits 8 +// kani-flags: -Z loop-contracts -Z mem-predicates -Z unstable-options --cbmc-args --object-bits 8 //! Check if loop contracts are correctly applied. diff --git a/tests/expected/object-bits/insufficient/expected b/tests/expected/object-bits/insufficient/expected index e673cf9f6c98..573a8db8db7e 100644 --- a/tests/expected/object-bits/insufficient/expected +++ b/tests/expected/object-bits/insufficient/expected @@ -1 +1 @@ -too many addressed objects: maximum number of objects is set to 2^n=32 (with n=5); use the `--enable-unstable --cbmc-args --object-bits n` option to increase the maximum number +too many addressed objects: maximum number of objects is set to 2^n=32 (with n=5); use the `-Z unstable-options --cbmc-args --object-bits n` option to increase the maximum number diff --git a/tests/expected/object-bits/insufficient/main.rs b/tests/expected/object-bits/insufficient/main.rs index 4da74190cb21..ad11d20e71c3 100644 --- a/tests/expected/object-bits/insufficient/main.rs +++ b/tests/expected/object-bits/insufficient/main.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --default-unwind 30 --enable-unstable --cbmc-args --object-bits 5 +// kani-flags: --default-unwind 30 -Z unstable-options --cbmc-args --object-bits 5 //! Checks for error message with an --object-bits value that is too small //! Use linked list to ensure that each member represents a new object. diff --git a/tests/expected/unwind-flags-conflict/main.rs b/tests/expected/unwind-flags-conflict/main.rs index f6d018a8d947..d1210d5d1448 100644 --- a/tests/expected/unwind-flags-conflict/main.rs +++ b/tests/expected/unwind-flags-conflict/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --default-unwind 2 --enable-unstable --cbmc-args --unwindset 2 +// kani-flags: --default-unwind 2 -Z unstable-options --cbmc-args --unwindset 2 #[kani::proof] fn main() {} diff --git a/tests/firecracker/virtio-balloon-compact/ignore-main.rs b/tests/firecracker/virtio-balloon-compact/ignore-main.rs index 09730a316490..01e298856b64 100644 --- a/tests/firecracker/virtio-balloon-compact/ignore-main.rs +++ b/tests/firecracker/virtio-balloon-compact/ignore-main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// Try with: kani ignore-main.rs --default-unwind 3 --enable-unstable --cbmc-args --object-bits 11 +// Try with: kani ignore-main.rs --default-unwind 3-Z unstable-options --cbmc-args --object-bits 11 // With kissat as the solver (--external-sat-solver /path/to/kissat) this takes ~5mins pub const MAX_PAGE_COMPACT_BUFFER: usize = 2048; diff --git a/tests/kani/DynTrait/any_cast_int.rs b/tests/kani/DynTrait/any_cast_int.rs index dfbb025796d7..2f7b7fa3a28d 100644 --- a/tests/kani/DynTrait/any_cast_int.rs +++ b/tests/kani/DynTrait/any_cast_int.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --no-restrict-vtable +// kani-flags: --no-restrict-vtable -Z restrict-vtable // Tracking issue for the need for this flag: // https://github.com/model-checking/kani/issues/802 diff --git a/tests/kani/DynTrait/vtable_restrictions.rs b/tests/kani/DynTrait/vtable_restrictions.rs index 0aba65bd022d..d73d68786285 100644 --- a/tests/kani/DynTrait/vtable_restrictions.rs +++ b/tests/kani/DynTrait/vtable_restrictions.rs @@ -5,7 +5,7 @@ // FIXME until the corresponding CBMC path lands: -// kani-flags: --enable-unstable --restrict-vtable +// kani-flags: -Z restrict-vtable struct Sheep {} struct Cow {} diff --git a/tests/kani/Overflow/pointer_overflow_fail.rs b/tests/kani/Overflow/pointer_overflow_fail.rs index 0ed5a61e8582..91c7c3707199 100644 --- a/tests/kani/Overflow/pointer_overflow_fail.rs +++ b/tests/kani/Overflow/pointer_overflow_fail.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --extra-pointer-checks +// kani-flags:-Z unstable-options --extra-pointer-checks // kani-verify-fail #[kani::proof] diff --git a/tests/ui/concrete-playback/array/main.rs b/tests/ui/concrete-playback/array/main.rs index a04688469c08..a2230874e920 100644 --- a/tests/ui/concrete-playback/array/main.rs +++ b/tests/ui/concrete-playback/array/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] #[kani::unwind(10)] diff --git a/tests/ui/concrete-playback/bool/main.rs b/tests/ui/concrete-playback/bool/main.rs index 43261acf7636..2a96dfe9cedc 100644 --- a/tests/ui/concrete-playback/bool/main.rs +++ b/tests/ui/concrete-playback/bool/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/cover/main.rs b/tests/ui/concrete-playback/cover/main.rs index 2e732b352d6a..58d5d9662691 100644 --- a/tests/ui/concrete-playback/cover/main.rs +++ b/tests/ui/concrete-playback/cover/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/custom/main.rs b/tests/ui/concrete-playback/custom/main.rs index 44d7143addb0..730b1b34ade8 100644 --- a/tests/ui/concrete-playback/custom/main.rs +++ b/tests/ui/concrete-playback/custom/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print struct MyStruct { field1: u8, diff --git a/tests/ui/concrete-playback/f32/main.rs b/tests/ui/concrete-playback/f32/main.rs index 6917bff32ba5..6bd15fa7b750 100644 --- a/tests/ui/concrete-playback/f32/main.rs +++ b/tests/ui/concrete-playback/f32/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print /// Note: Don't include NaN because there are multiple possible NaN values. #[kani::proof] diff --git a/tests/ui/concrete-playback/f64/main.rs b/tests/ui/concrete-playback/f64/main.rs index 03475ac71685..7809ac53bc71 100644 --- a/tests/ui/concrete-playback/f64/main.rs +++ b/tests/ui/concrete-playback/f64/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print /// Note: Don't include NaN because there are multiple possible NaN values. #[kani::proof] diff --git a/tests/ui/concrete-playback/i128/main.rs b/tests/ui/concrete-playback/i128/main.rs index 44adc7d4ee1a..f2453ca58418 100644 --- a/tests/ui/concrete-playback/i128/main.rs +++ b/tests/ui/concrete-playback/i128/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/i16/main.rs b/tests/ui/concrete-playback/i16/main.rs index dc4c105cf390..bac46f62eb36 100644 --- a/tests/ui/concrete-playback/i16/main.rs +++ b/tests/ui/concrete-playback/i16/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/i32/main.rs b/tests/ui/concrete-playback/i32/main.rs index 02adef43dfe5..698a620f9b23 100644 --- a/tests/ui/concrete-playback/i32/main.rs +++ b/tests/ui/concrete-playback/i32/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/i64/main.rs b/tests/ui/concrete-playback/i64/main.rs index f441a83dc227..cf8533dd4954 100644 --- a/tests/ui/concrete-playback/i64/main.rs +++ b/tests/ui/concrete-playback/i64/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/i8/main.rs b/tests/ui/concrete-playback/i8/main.rs index 0c3c919dfa11..a61b1fe92612 100644 --- a/tests/ui/concrete-playback/i8/main.rs +++ b/tests/ui/concrete-playback/i8/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/isize/main.rs b/tests/ui/concrete-playback/isize/main.rs index c14501c0f4bc..47fb3a55f6b2 100644 --- a/tests/ui/concrete-playback/isize/main.rs +++ b/tests/ui/concrete-playback/isize/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/mult-harnesses/main.rs b/tests/ui/concrete-playback/mult-harnesses/main.rs index df4278327e2e..9ec9b4593b91 100644 --- a/tests/ui/concrete-playback/mult-harnesses/main.rs +++ b/tests/ui/concrete-playback/mult-harnesses/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print //! Multiple harnesses with the same name but under different modules. diff --git a/tests/ui/concrete-playback/non_zero/main.rs b/tests/ui/concrete-playback/non_zero/main.rs index 24534ff65adb..e8637b06e4e3 100644 --- a/tests/ui/concrete-playback/non_zero/main.rs +++ b/tests/ui/concrete-playback/non_zero/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print use std::num::NonZeroU8; diff --git a/tests/ui/concrete-playback/option/main.rs b/tests/ui/concrete-playback/option/main.rs index f882b63654e5..63a9981e6d67 100644 --- a/tests/ui/concrete-playback/option/main.rs +++ b/tests/ui/concrete-playback/option/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/result/main.rs b/tests/ui/concrete-playback/result/main.rs index 944127022be1..ee8c85ffb1b1 100644 --- a/tests/ui/concrete-playback/result/main.rs +++ b/tests/ui/concrete-playback/result/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/slice-formula/main.rs b/tests/ui/concrete-playback/slice-formula/main.rs index 3739eb2e90b0..e6c91179204c 100644 --- a/tests/ui/concrete-playback/slice-formula/main.rs +++ b/tests/ui/concrete-playback/slice-formula/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print //! We explicitly don't check what concrete values are returned for `_u8_1` and `_u8_3` as they could be anything. //! In practice, though, they will likely be 0. diff --git a/tests/ui/concrete-playback/u128/main.rs b/tests/ui/concrete-playback/u128/main.rs index e2de702c5b74..727fd4ee3f2a 100644 --- a/tests/ui/concrete-playback/u128/main.rs +++ b/tests/ui/concrete-playback/u128/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/u16/main.rs b/tests/ui/concrete-playback/u16/main.rs index 108a7f95b90d..df925e658717 100644 --- a/tests/ui/concrete-playback/u16/main.rs +++ b/tests/ui/concrete-playback/u16/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/u32/main.rs b/tests/ui/concrete-playback/u32/main.rs index 9193b2dfaff2..52ffad6c5547 100644 --- a/tests/ui/concrete-playback/u32/main.rs +++ b/tests/ui/concrete-playback/u32/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/u64/main.rs b/tests/ui/concrete-playback/u64/main.rs index ec1fb67b9c6c..35eec405bf0b 100644 --- a/tests/ui/concrete-playback/u64/main.rs +++ b/tests/ui/concrete-playback/u64/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/u8/main.rs b/tests/ui/concrete-playback/u8/main.rs index d05095b7b05c..6bde754a7a81 100644 --- a/tests/ui/concrete-playback/u8/main.rs +++ b/tests/ui/concrete-playback/u8/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/concrete-playback/unsupported/loop.rs b/tests/ui/concrete-playback/unsupported/loop.rs index 19424d084157..032eb70ab890 100644 --- a/tests/ui/concrete-playback/unsupported/loop.rs +++ b/tests/ui/concrete-playback/unsupported/loop.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] #[kani::unwind(2)] diff --git a/tests/ui/concrete-playback/usize/main.rs b/tests/ui/concrete-playback/usize/main.rs index c28e89d1c4cb..f74d6b0dc71a 100644 --- a/tests/ui/concrete-playback/usize/main.rs +++ b/tests/ui/concrete-playback/usize/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --concrete-playback=print +// kani-flags: -Zconcrete-playback --concrete-playback=print #[kani::proof] pub fn harness() { diff --git a/tests/ui/invalid-cbmc-function-arg/main.rs b/tests/ui/invalid-cbmc-function-arg/main.rs index 978678359b67..139d4b1695e2 100644 --- a/tests/ui/invalid-cbmc-function-arg/main.rs +++ b/tests/ui/invalid-cbmc-function-arg/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable +// kani-flags: -Z unstable-options // cbmc-flags: --function main //! This testcase is to ensure that user cannot pass --function as cbmc-flags diff --git a/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs b/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs index aa49e7c93d95..98aef85e34c8 100644 --- a/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs +++ b/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --synthesize-loop-contracts +// kani-flags: -Z unstable-options --synthesize-loop-contracts // Check if goto-synthesizer is correctly called, and synthesizes the required // loop invariants. diff --git a/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs index 3a1302111b32..2819a35efd9b 100644 --- a/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs +++ b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --synthesize-loop-contracts --cbmc-args --object-bits 4 +// kani-flags: -Z unstable-options --synthesize-loop-contracts --cbmc-args --object-bits 4 // Check if goto-synthesizer is correctly called, and synthesizes the required // loop invariants. diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 36a83a94e23e..d31e895eab6f 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -308,7 +308,7 @@ impl TestCx<'_> { kani.arg(&self.testpaths.file).args(&self.props.kani_flags); if !self.props.cbmc_flags.is_empty() { - kani.arg("--enable-unstable").arg("--cbmc-args").args(&self.props.cbmc_flags); + kani.arg("-Zunstable-options").arg("--cbmc-args").args(&self.props.cbmc_flags); } self.compose_and_run(kani)