prusti-dev
prusti-dev copied to clipboard
Consistency error with chained pure fns and tuples
The following runs into a Consistency error: Local variable _1 not found. when verifying the main function:
use prusti_contracts::*;
#[pure]
pub fn zero() -> usize { 0 }
#[pure]
pub fn tpl() -> (usize, usize) {
(zero(), zero())
}
fn main() {
let (a, b) = tpl();
}
In the above, tpl (as used in main) is encoded as:
function m_tpl__$TY$__(): Snap$tuple2$usize$usize
requires true
requires true
ensures true
ensures [result == mirror_simple$m_tpl__$TY$__(), true]
{
cons$0$__$TY$__Snap$tuple2$usize$usize$(_1.val_int, _2.val_int)
}
Ignoring the superfluous lines of true, somehow the call to zero() fails to be included and _1/_2 are never set.
Is this check causing the interpreter to skip the assignment?
https://github.com/viperproject/prusti-dev/blob/7977d30a028edfe0e300bb2931992d4029385b41/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs#L851