Skip to content

Commit dac47af

Browse files
authored
fix: set x86 as verification target (#36)
1 parent 00d9bc7 commit dac47af

2 files changed

Lines changed: 10 additions & 2 deletions

File tree

src/toolchain.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ struct ToolchainConfig {
1414
struct Toolchain {
1515
channel: String,
1616
components: Option<Vec<String>>,
17+
targets: Option<Vec<String>>,
1718
}
1819

1920
impl ToolchainConfig {

src/verus.rs

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ pub type DynError = Box<dyn std::error::Error>;
2626
2727
pub const CARGO_VERUS_BIN: &str = "cargo-verus";
2828
pub const CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH";
29+
pub const VERIFICATION_RUST_TARGET: &str = "x86_64-unknown-none";
2930

3031
pub const VERUS_HINT_RELEASE: &str = "tools/verus/source/target-verus/release";
3132
pub const VERUS_HINT: &str = "tools/verus/source/target-verus/debug";
@@ -613,13 +614,15 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
613614
let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
614615
let ts_start = Instant::now();
615616
let cmd = &mut Command::new(get_cargo_verus(options.release));
616-
cmd.arg(if options.focus { "focus" } else { "verify" });
617+
cmd.env("RUSTC_BOOTSTRAP", "1")
618+
.arg(if options.focus { "focus" } else { "verify" });
617619
if !options.focus && verus_args_should_apply_to_roots_only(&options.pass_through) {
618620
cmd.arg("--fwd-verus-args-to").arg("roots");
619621
}
620622
if let Some(target) = target {
621623
cmd.arg("-p").arg(&target.name);
622624
}
625+
cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
623626

624627
let mut verus_args = Vec::new();
625628
if options.log {
@@ -864,13 +867,17 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> {
864867
pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
865868
let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
866869
let cmd = &mut Command::new(get_cargo_verus(options.release));
867-
cmd.arg("build");
870+
cmd.env("RUSTC_BOOTSTRAP", "1").arg("build");
871+
if verus_args_should_apply_to_roots_only(&options.pass_through) {
872+
cmd.arg("--fwd-verus-args-to").arg("roots");
873+
}
868874
if let Some(target) = target {
869875
cmd.arg("-p").arg(&target.name);
870876
}
871877
if options.release {
872878
cmd.arg("--release");
873879
}
880+
cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
874881

875882
let mut verus_args = Vec::new();
876883
if options.log {

0 commit comments

Comments
 (0)