diff --git a/source/cargo-verus/src/main.rs b/source/cargo-verus/src/main.rs index 5bc2dc1e8c..a6cd9a876c 100644 --- a/source/cargo-verus/src/main.rs +++ b/source/cargo-verus/src/main.rs @@ -54,6 +54,17 @@ fn show_version() { println!("{version_info}"); } +fn process(args: &[String]) -> Result<(), i32> { + let cmd = VerusCmd::new(args); + + let mut cmd = cmd.into_std_cmd(); + + let exit_status = + cmd.spawn().expect("could not run cargo").wait().expect("failed to wait for cargo?"); + + if exit_status.success() { Ok(()) } else { Err(exit_status.code().unwrap_or(-1)) } +} + struct VerusCmd { cargo_subcommand: CargoSubcommand, cargo_args: Vec, @@ -130,20 +141,20 @@ impl VerusCmd { } fn into_std_cmd(self) -> Command { - let common_verus_driver_args = - pack_verus_driver_args_for_env(self.common_verus_driver_args.iter()); - let mut cmd = Command::new(env::var("CARGO").unwrap_or("cargo".into())); - cmd.env("RUSTC_WRAPPER", checked_verus_driver_path()) - .arg(self.cargo_subcommand.to_arg().to_owned()) - .args(&self.cargo_args); + cmd.arg(self.cargo_subcommand.to_arg().to_owned()).args(&self.cargo_args); + + cmd.env("RUSTC_WRAPPER", checked_verus_driver_path()); cmd.env("__VERUS_DRIVER_VIA_CARGO__", "1"); // See https://github.com/rust-lang/cargo/blob/94aa7fb1321545bbe922a87cb11f5f4559e3be63/src/cargo/core/compiler/fingerprint/mod.rs#L71 cmd.env("__CARGO_DEFAULT_LIB_METADATA", "verus"); + let common_verus_driver_args = + pack_verus_driver_args_for_env(self.common_verus_driver_args.iter()); + if !common_verus_driver_args.is_empty() { cmd.env("__VERUS_DRIVER_ARGS__", common_verus_driver_args); } @@ -211,17 +222,6 @@ impl VerusCmd { } } -fn process(args: &[String]) -> Result<(), i32> { - let cmd = VerusCmd::new(args); - - let mut cmd = cmd.into_std_cmd(); - - let exit_status = - cmd.spawn().expect("could not run cargo").wait().expect("failed to wait for cargo?"); - - if exit_status.success() { Ok(()) } else { Err(exit_status.code().unwrap_or(-1)) } -} - fn filter_args( mut orig_args: impl Iterator>, standalone_flags: &[impl AsRef], diff --git a/source/verus-driver/src/main.rs b/source/verus-driver/src/main.rs index f871b2c34a..01373f33b8 100644 --- a/source/verus-driver/src/main.rs +++ b/source/verus-driver/src/main.rs @@ -13,6 +13,7 @@ use std::io::Read; use std::mem; use std::path::{Path, PathBuf}; use std::process::exit; +use std::sync::atomic::AtomicBool; use std::sync::Arc; use rustc_driver::{Callbacks, RunCompiler}; @@ -48,7 +49,7 @@ pub fn main() { handler.note(format!("Verus version: {version_info}")); }) } else { - std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false)) + Arc::new(AtomicBool::new(false)) }; exit(rustc_driver::catch_with_exit_code(move || { @@ -218,6 +219,12 @@ pub fn main() { } } + let mut import_deps_if_present = parsed_verus_driver_inner_args + .import_dep_if_present + .iter() + .cloned() + .collect::>(); + let mut externs = BTreeMap::>::new(); for (key, entry) in orig_rustc_opts.externs.iter() { @@ -233,12 +240,6 @@ pub fn main() { } } - let mut import_deps_if_present = parsed_verus_driver_inner_args - .import_dep_if_present - .iter() - .cloned() - .collect::>(); - if let Some(verus_sysroot) = parsed_verus_driver_inner_args .verus_sysroot .or_else(|| dep_tracker.get_env("VERUS_SYSROOT"))