Remove --visualize and cbmc-viewer call

kani-driver/src/args/mod.rs

@@ -129,19 +129,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true, requires("enable_unstable"))]
     pub assess: bool,
 
-    /// Generate visualizer report to `<target-dir>/report/html/index.html`
-    #[arg(long)]
-    pub visualize: bool,
     /// Generate concrete playback unit test.
     /// If value supplied is 'print', Kani prints the unit test to stdout.
     /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
     /// This option does not work with `--output-format old`.
-    #[arg(
-        long,
-        conflicts_with_all(&["visualize"]),
-        ignore_case = true,
-        value_enum
-    )]
+    #[arg(long, ignore_case = true, value_enum)]
     pub concrete_playback: Option<ConcretePlaybackMode>,
     /// Keep temporary files generated throughout Kani process. This is already the default
     /// behavior for `cargo-kani`.
@@ -315,9 +307,9 @@ impl VerificationArgs {
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
 
-    /// Assertion reachability checks should be disabled when running with --visualize
+    /// Assertion reachability checks should be disabled
     pub fn assertion_reach_checks(&self) -> bool {
-        !self.no_assertion_reach_checks && !self.visualize
+        !self.no_assertion_reach_checks
     }
 
     /// Suppress our default value, if the user has supplied it explicitly in --cbmc-args
@@ -532,18 +524,6 @@ impl ValidateArgs for VerificationArgs {
             );
         }
 
-        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 {
             print_obsolete(&self.common_args, "--mir-linker");
         }

kani-driver/src/call_cbmc.rs

@@ -75,7 +75,8 @@ impl KaniSession {
             }
         } else {
             // Add extra argument to receive the output in JSON format.
-            // Done here because `--visualize` uses the XML format instead.
+            // Done here because now removed `--visualize` used the XML format instead.
+            // TODO: move this now that we don't use --visualize
             cmd.arg("--json-ui");
 
             // Spawn the CBMC process and process its output below
@@ -138,10 +139,7 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize
-            && self.args.concrete_playback.is_none()
-            && !self.args.no_slice_formula
-        {
+        if self.args.concrete_playback.is_none() && !self.args.no_slice_formula {
             args.push("--slice-formula".into());
         }
 

kani-driver/src/harness_runner.rs

@@ -52,8 +52,6 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
             sorted_harnesses
                 .par_iter()
                 .map(|harness| -> Result<HarnessResult<'pr>> {
-                    let harness_filename = harness.pretty_name.replace("::", "-");
-                    let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
                     let goto_file =
                         self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
 
@@ -63,7 +61,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
                         self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?;
                     }
 
-                    let result = self.sess.check_harness(goto_file, &report_dir, harness)?;
+                    let result = self.sess.check_harness(goto_file, harness)?;
                     Ok(HarnessResult { harness, result })
                 })
                 .collect::<Result<Vec<_>>>()
@@ -105,35 +103,28 @@ impl KaniSession {
     pub(crate) fn check_harness(
         &self,
         binary: &Path,
-        report_dir: &Path,
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
         if !self.args.common_args.quiet {
             println!("Checking harness {}...", harness.pretty_name);
         }
 
-        if self.args.visualize {
-            self.run_visualize(binary, report_dir, harness)?;
-            // Strictly speaking, we're faking success here. This is more "no error"
-            Ok(VerificationResult::mock_success())
-        } else {
-            let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
+        let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-            // When quiet, we don't want to print anything at all.
-            // When output is old, we also don't have real results to print.
-            if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
-                println!(
-                    "{}",
-                    result.render(
-                        &self.args.output_format,
-                        harness.attributes.should_panic,
-                        self.args.coverage
-                    )
-                );
-            }
-            self.gen_and_add_concrete_playback(harness, &mut result)?;
-            Ok(result)
+        // When quiet, we don't want to print anything at all.
+        // When output is old, we also don't have real results to print.
+        if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
+            println!(
+                "{}",
+                result.render(
+                    &self.args.output_format,
+                    harness.attributes.should_panic,
+                    self.args.coverage
+                )
+            );
         }
+        self.gen_and_add_concrete_playback(harness, &mut result)?;
+        Ok(result)
     }
 
     /// Concludes a session by printing a summary report and exiting the process with an
@@ -159,7 +150,7 @@ impl KaniSession {
         }
 
         // We currently omit a summary if there was just 1 harness
-        if !self.args.common_args.quiet && !self.args.visualize {
+        if !self.args.common_args.quiet {
             if failing > 0 {
                 println!("Summary:");
             }

kani-driver/src/main.rs

@@ -22,7 +22,6 @@ mod args_toml;
 mod assess;
 mod call_cargo;
 mod call_cbmc;
-mod call_cbmc_viewer;
 mod call_goto_cc;
 mod call_goto_instrument;
 mod call_goto_synthesizer;

kani-driver/src/project.rs

@@ -32,6 +32,8 @@ pub struct Project {
     pub metadata: Vec<KaniMetadata>,
     /// The directory where all outputs should be directed to. This path represents the canonical
     /// version of outdir.
+    /// NOTE: This needs to be marked as dead_code even when it's clearly not
+    #[allow(dead_code)]
     pub outdir: PathBuf,
     /// The collection of artifacts kept as part of this project.
     artifacts: Vec<Artifact>,