viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.55k stars 106 forks source link

Windows executable crashes during verification #1390

Open Patrick-6 opened 1 year ago

Patrick-6 commented 1 year ago

Running the latest Prusti nightly release (v-2023-04-05-1606) (and also some of the previous releases) on Windows 10 in Powershell or Cmd results in the following error at the end of the verification:

$ cargo-prusti
Compiling libc v0.2.141
Compiling proc-macro2 v1.0.56
Compiling quote v1.0.26
Compiling unicode-ident v1.0.8
Compiling syn v1.0.109
Compiling cfg-if v1.0.0
Compiling either v1.8.1
Compiling rustc-hash v1.1.0
Compiling itertools v0.10.5
Compiling getrandom v0.2.8
Compiling uuid v1.3.0
Compiling prusti-specs v0.1.6
Compiling prusti-contracts-proc-macros v0.1.6
Checking prusti-contracts v0.1.6
Checking prusti_tests v0.1.0 (prusti_tests) 

error: could not compile `prusti_tests`                                                                                                                                                                                                                                                                                                                                                     Caused by: process didn't exit successfully:
`prusti-rustc.exe --crate-name prusti_tests --edition=2021 src\main.rs --error-format=json
--json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=189 --crate-type bin
--emit=dep-info,metadata -C embed-bitcode=no -C debuginfo=2 -C metadata=47ec84627cf201b7
-C extra-filename=-47ec84627cf201b7 --out-dir prusti_tests\target\verify\debug\deps
-C incremental=prusti_tests\target\verify\debug\incremental -L dependency=prusti_tests\target\verify\debug\deps
--extern prusti_contracts=prusti_tests\target\verify\debug\deps\libprusti_contracts-a1424841f29834d4.rmeta`

(exit code: 0xc0000005, STATUS_ACCESS_VIOLATION)

This error appears even when verifying a crate with almost no code in lib.rs:

use prusti_contracts::*;

#[requires(true)]
fn _test() {}

Running cargo-prusti through Prusti-Assistant (using the local build channel) seems to work without showing the error message in the output.

I also ran the Ubuntu 22.04 executable for the same Prusti release on WSL with the same crate, and it passed without any issues.