From 18df9ec15306f074aa463da3532e8aa837ed77b4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 21 Jun 2024 12:07:13 -0700 Subject: [PATCH] Deprecate `--visualize` in favor of concrete playback We believe the `--visualize` is much harder to use than concrete playback. In the rare cases where a trace might be relevant, users can still use CBMC trace. For most users, this will simplify instalation since Kani will no longer require python. --- kani-driver/src/args/mod.rs | 14 +++++++++----- tests/cargo-kani/simple-visualize/main.expected | 1 + 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index f0c9cb0c4e8d..b73777622ee9 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -542,12 +542,16 @@ impl ValidateArgs for VerificationArgs { ); } - if self.visualize && !self.common_args.enable_unstable { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "Missing argument: --visualize now requires --enable-unstable + if self.visualize { + if !self.common_args.enable_unstable { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "Missing argument: --visualize now requires --enable-unstable due to open issues involving incorrect results.", - )); + )); + } else { + print_deprecated(&self.common_args, "--visualize", "--concrete-playback"); + } } if self.mir_linker { diff --git a/tests/cargo-kani/simple-visualize/main.expected b/tests/cargo-kani/simple-visualize/main.expected index a863a195a4ff..1d0839175310 100644 --- a/tests/cargo-kani/simple-visualize/main.expected +++ b/tests/cargo-kani/simple-visualize/main.expected @@ -1 +1,2 @@ +warning: The `--visualize` option is deprecated. This option will be removed soon. Consider using `--concrete-playback` instead report-main/html/index.html