-
Notifications
You must be signed in to change notification settings - Fork 121
Open
Description
I am trying to run Prusti from VS Code, and get the following error:
Run command 'c:\Users\<user>\AppData\Roaming\Code\User\globalStorage\viper-admin.prusti-assistant\prustiTools\Latest\prusti\cargo-prusti.exe --message-format=json'
Spawned PID: 19380
Output from 'c:\Users\<user>\AppData\Roaming\Code\User\globalStorage\viper-admin.prusti-assistant\prustiTools\Latest\prusti\cargo-prusti.exe --message-format=json' (0.7s):
┌──── Begin stdout ────┐
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking hello_world v0.1.0 (C:\Users\<user>\projects\trust_rust)
[2025-07-22T16:49:54Z INFO prusti_driver] Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:29:52 UTC
[2025-07-22T16:49:54Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2025-07-22T16:49:54Z INFO prusti_viper::verifier] - average (hello_world::average)
[2025-07-22T16:49:54Z INFO prusti_viper::verifier] Source: src\main.rs:2:1: 2:38 (#0)
[2025-07-22T16:49:54Z INFO prusti_viper::verifier] - main (hello_world::main)
[2025-07-22T16:49:54Z INFO prusti_viper::verifier] Source: src\main.rs:8:1: 8:10 (#0)
[2025-07-22T16:49:54Z INFO prusti_viper::encoder::encoder] Encoding: hello_world::average (hello_world::average)
[2025-07-22T16:49:54Z INFO prusti_viper::encoder::encoder] Encoding: hello_world::main (hello_world::main)
[2025-07-22T16:49:54Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.013 seconds)
[2025-07-22T16:49:54Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2025-07-22T16:49:54Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.000 seconds)
[2025-07-22T16:49:54Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2025-07-22T16:49:54Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:51549
thread 'rustc' panicked at prusti-viper\src\verifier.rs:265:21:
Verification request of program hello_world::average failed: reqwest::Error { kind: Request, url: Url { scheme: "http", cannot_be_a_base: false, username: "", password: None, host: Some(Domain("localhost")), port: Some(51549), path: "/bincode/verify/", query: None, fragment: None }, source: hyper::Error(IncompleteMessage) }
stack backtrace:
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: the compiler unexpectedly panicked. this is a bug.
note: we would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
warning: the ICE couldn't be written to `c:\Users\<user>\projects\trust_rust\rustc-ice-2025-07-22T16:49:54.5993829Z-17644.txt`: The filename, directory name, or volume label syntax is incorrect. (os error 123)
note: rustc 1.74.0-nightly (ca2b74f1a 2023-09-14) running on x86_64-pc-windows-msvc
note: compiler flags: --crate-type bin -C embed-bitcode=no -C debuginfo=2 -C incremental=[REDACTED]
note: some of the compiler flags provided by cargo are hidden
query stack during panic:
end of query stack
note: Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:29:52 UTC
[2025-07-22T16:49:55Z INFO prusti_utils::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (0.417 seconds)
[2025-07-22T16:49:55Z INFO prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.453 seconds)
error: could not compile `hello_world` (bin "hello_world")
└──── End stderr ──────┘
Exit code 101, signal null.
Metadata
Metadata
Assignees
Labels
No labels