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

Internal error from multiple pledges per function

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

Having multiple pledges (assert_on_expiry or after_expiry) on a single function causes an internal error, but it should be a proper error:

use prusti_contracts::*;

#[after_expiry(true)]
#[assert_on_expiry(true, true)]
fn _test(x: &mut i32) -> &mut i32 {
    x
}

Error:

thread 'rustc' panicked at 'There can be at most one pledge in the function postcondition.', prusti-viper\src\encoder\procedure_encoder.rs:4152:13
stack backtrace:
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:36:11 UTC

Patrick-6 avatar Feb 14 '23 17:02 Patrick-6