From 73843ecd605be634c56b4c3f8316090cc3bf36f2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 21 Jun 2024 12:48:38 -0700 Subject: [PATCH] Deprecate `--visualize` in favor of concrete playback (#3281) 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 installation since Kani will no longer depend on Python3. Note: As opposed to `--function` which was purely an internal feature, I believe we have mentioned `--visualize` to users before, so I think it's important to have a deprecation period. Related #2832 --- 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 5c23a7358caf6..4c0fe98cc65d6 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -532,12 +532,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 a863a195a4ff2..1d08391753108 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