prusti-dev
prusti-dev copied to clipboard
Prusti fails to compile a crate when it's part of a larger project
I'm not sure what's happening here because I though Prusti verified at the modularity of crates, but this exact code is verified in an independent crate. But when this crate is part of a larger repository (https://github.com/theseus-os/Theseus), Prusti fails to compile the crate.
#![no_std]
extern crate prusti_contracts;
use prusti_contracts::*;
#[ensures(result >= a)]
#[ensures(result >= b)]
fn max(a: u32, b: u32) -> u32 {
if a > b {
a
} else {
b
}
}
This is the Prusti Assistant output:
Run verification on /home/ramla/Theseus/kernel/chunk1/src/lib.rs...
Preparing verification run #17.
Killing 0 processes.
Run command '/home/ramla/prusti-release-ubuntu/cargo-prusti --message-format=json'
Spawned PID: 8797
Output from '/home/ramla/prusti-release-ubuntu/cargo-prusti --message-format=json' (0.3s):
┌──── Begin stdout ────┐
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking chunk1 v0.1.0 (/home/ramla/Theseus/kernel/chunk1)
[2022-07-27T20:41:48Z WARN prusti_driver] Specifications are supported only from 2018 edition. Please specify the edition with adding a command line argument `--edition=2018` or `--edition=2021`.
[2022-07-27T20:41:48Z INFO prusti_driver] Prusti version: commit 4dfd34d 2021-11-22 16:35:31 UTC, built on 2021-11-22 16:40:49 UTC
error: unknown `--json` option `future-incompat`
error: could not compile `chunk1`
└──── End stderr ──────┘
Exit code 101, signal null.
The verification failed, but there are no errors to report.
Prusti encountered an unexpected error. We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See the log (View -> Output -> Prusti Assistant) for more details.
I do not think we support cargo workspaces. @fpoli Can you confirm?
I'm not aware of limitations regarding cargo workspaces. Prusti should just run on each crate that compose the workspace, but not on the crates.io dependencies.
The "error: unknown '--json' option 'future-incompat'" look the same as #1149. Did you install rustup
via snap? If so, see this answer: https://stackoverflow.com/a/72168145/2491528.
Closing as duplicate of #1149. This issue should now be fixed on master.