Deprecate --visualize in favor of concrete playback (rust-lang#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 rust-lang#2832

Author: celinval

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 {

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