prusti-dev
prusti-dev copied to clipboard
No counterexample for `prusti_assert`
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: ?