cargo-prusti ignores specification

[fpoli]

I tried running cargo-prusti on the following crate:

Cargo.toml:

[package]
name = "example"
version = "0.1.0"
edition = "2018"

[dependencies]
prusti-contracts = { git = "https://github.com/viperproject/prusti-dev.git" }

src/main.rs:

use prusti_contracts::*;

#[requires(x > 123)]
fn test(x: i32) {
    assert!(x > 123);
}

fn main() {
    assert!(true);
}

However, the assertion in the test function does not verify and Prusti reports an error. I checked the Viper dump and the x > 123 precondition is not assumed at the beginning of the function, but it should be. I suspect that for some reason all specifications are ignored while running cargo-prusti. Maybe this is related to the cfg(prusti) compilation flag.

This issue also shows that cargo-prusti is not properly tested. We really need #3.

[fpoli]

This is actually an unsoundness of cargo-prusti, because by ignoring specifications it doesn't generate verification errors for e.g. the following program reported by @rishitc. prusti-rustc and the Prusti IDE don't have this issue.

#![allow(unused)]
fn main() {
    extern crate prusti_contracts;
    use prusti_contracts::*;

    #[ensures((result == a && result != b) || (result == a && result == b))]
    fn max(a: i32, b: i32) -> i32 {
        if a > b {
            a
        } else {
            b
        }
    }
}