Prusti doesn’t run for the thumbv7em-none-eabihf target

[pwnorbitals]

(new user here)
The rest of the project is well-configured, but it seems that Prusti is compiling in some kind of isolated environment and doesn’t take cross-compilation into account when running the Rust compiler.

Typical output:

[fpoli]

Could you describe how to reproduce this issue? Do you run cargo prusti or something different?

[fpoli]

Prusti by default uses the sysroot of the nightly rustc version specified in Prusti's repository. The RUST_SYSROOT environment variable can be used to force Prusti to use a different sysroot. Maybe that allows Prusti to work when cross-compiling, but we never tested this use case.

[pwnorbitals]

Could you describe how to reproduce this issue? Do you run cargo prusti or something different?

I used the Prusti extension in VSCode. I unfortunately couldn't get cargo prusti to run in my WSL machine for some reason

[pwnorbitals]

Prusti by default uses the sysroot of the nightly rustc version specified in Prusti's repository. The RUST_SYSROOT environment variable can be used to force Prusti to use a different sysroot. Maybe that allows Prusti to work when cross-compiling, but we never tested this use case.

I understand, but this means all user configuration that allow their project to work will be lost. Cross-compilation requires the toolchain and linker, which you can't really have in this case. Does Prusti absolutely need a sysroot ?

[fpoli]

cargo prusti and the IDE extension should ideally always work out of the box (i.e. in any situation where cargo clippy works), so what you reported is a bug in how Prusti interacts with the compiler. If I recall correctly, the sysroot is required by rustc, otherwise it'll not find the core/std libraries. Our decision of forcing a fixed Rust toolchain is very old; it's possible that we did that just to workaround some early issue and then forgot about it. If manually setting RUST_SYSROOT works for you, then we can easily remove the hardcoded toolchain version from Prusti. All the related code is here, and it should be enough to change 3 lines. The RUST_SYSROOT can be configured in the settings of the Prusti extension on VS Code. There is a prusti-assistant.extraPrustiEnv field that should be good enough.