prusti-dev
prusti-dev copied to clipboard
Internal error from multiple pledges per function
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