Use <target>/kani as the target directory and clean at every build (r…

…ust-lang#1847)

We can't really handle caching compilation artifacts today. So we are going to perform a cargo clean before building the goto program. I also changed our target to use the kani subfolder inside target.

kani-driver/src/call_cargo.rs

@@ -6,6 +6,7 @@ use crate::session::{KaniSession, ReachabilityMode};
 use anyhow::{Context, Result};
 use cargo_metadata::{Metadata, MetadataCommand, Package};
 use std::ffi::OsString;
+use std::fs;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
@@ -32,9 +33,16 @@ impl KaniSession {
             .target_dir
             .as_ref()
             .unwrap_or(&metadata.target_directory.clone().into())
-            .clone();
+            .clone()
+            .join("kani");
         let outdir = target_dir.join(build_target).join("debug/deps");
 
+        // Clean directory before building since we are unable to handle cache today.
+        // TODO: https://github.com/model-checking/kani/issues/1736
+        if target_dir.exists() {
+            fs::remove_dir_all(&target_dir)?;
+        }
+
         let mut kani_args = self.kani_specific_flags();
         let rustc_args = self.kani_rustc_flags();
 

tests/output-files/check-output.sh

@@ -68,7 +68,7 @@ echo
 echo "Running multi-file check..."
 rm -rf build
 RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable --quiet
-cd build/${TARGET}/debug/deps/
+cd build/kani/${TARGET}/debug/deps/
 
 if ! [ -e cbmc-linked.for-main.c ]
 then