viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 102 forks source link

Internal error when assigning a closure call to a reference #1472

Open fpoli opened 8 months ago

fpoli commented 8 months ago

The program

fn main() {
    let mut a = 123;
    let x = &mut a;
    let gen = || { x };
    let y = gen(); // <-- ERROR
}

raises the internal error

Details: Type Closure(DefId(0:4 ~ 20231102_153740[9d5e]::main::{closure#0}), [i32, Binder(extern "RustCall" fn(()) -> &'?11 mut i32, []), (&'?12 mut i32,)]) can not be dereferenced