Skip to content

Commit 85635c6

Browse files
committed
fix: set x86 as verification target
1 parent 504e219 commit 85635c6

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
@@ -25,6 +25,7 @@ pub type DynError = Box<dyn std::error::Error>;
2525
2626
pub const CARGO_VERUS_BIN: &str = "cargo-verus";
2727
pub const CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH";
28+
pub const VERIFICATION_RUST_TARGET: &str = "x86_64-unknown-none";
2829

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

623626
let mut verus_args = Vec::new();
624627
if options.log {
@@ -758,13 +761,17 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> {
758761
pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
759762
let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
760763
let cmd = &mut Command::new(get_cargo_verus(options.release));
761-
cmd.arg("build");
764+
cmd.env("RUSTC_BOOTSTRAP", "1").arg("build");
765+
if verus_args_should_apply_to_roots_only(&options.pass_through) {
766+
cmd.arg("--fwd-verus-args-to").arg("roots");
767+
}
762768
if let Some(target) = target {
763769
cmd.arg("-p").arg(&target.name);
764770
}
765771
if options.release {
766772
cmd.arg("--release");
767773
}
774+
cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
768775

769776
let mut verus_args = Vec::new();
770777
if options.log {

0 commit comments

Comments
 (0)