prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Prusti fails to compile a crate when it's part of a larger project

Open Ramla-I opened this issue 2 years ago • 2 comments

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.

Ramla-I avatar Jul 27 '22 20:07 Ramla-I

I do not think we support cargo workspaces. @fpoli Can you confirm?

vakaras avatar Jul 29 '22 14:07 vakaras

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.

fpoli avatar Sep 19 '22 13:09 fpoli

Closing as duplicate of #1149. This issue should now be fixed on master.

fpoli avatar Oct 04 '22 09:10 fpoli