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

No counterexample for `prusti_assert`

Open Patrick-6 opened this issue 2 years ago • 0 comments

Asking Prusti to print counterexamples with counterexample = true works for assert and pre-/postcondition violations, but not for prusti_assert and its variants:

use prusti_contracts::*;

#[requires(_x >= 10)]
fn more_than_ten(_x: i32) {}

fn test_precondition(x: i32) {
    more_than_ten(x); // Counterexample printed
}

#[ensures(result >= 10)] // Counterexample printed
fn test_postcondition(x: i32) -> i32 {
    x
}

fn test_assert(x: i32) {
    assert!(x >= 10); // Counterexample printed
}

fn test_prusti_assert(x: i32) {
    prusti_assert!(x >= 10); // Counterexample NOT printed
}

fn test_prusti_assert_eq(x: i32) {
    prusti_assert_eq!(x, 10); // Counterexample NOT printed
}

fn test_prusti_assert_ne(x: i32) {
    prusti_assert_ne!(x, 10); // Counterexample NOT printed
}

For the working ones you get a message like this one:

[...]
assert_counterexample.rs(6, 22): counterexample for "x"
initial value: 9
final value: 9

But for the prusti_asserts you get:

[...]
assert_counterexample.rs(14, 23): counterexample for "x"
initial value: ?
final value: ?

Patrick-6 avatar Mar 08 '23 12:03 Patrick-6