creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

Pattern in closure argument sometimes generate incorrect coma code #1118

Open arnaudgolfouse opened 1 day ago

arnaudgolfouse commented 1 day ago

The following code generate incorrect coma:

pub fn f() {
    let _ = |&x: &i32| x;
}

Indeed the line use M_result_in_spec__f__blabla_Type as Closure'0 is present inside module M_result_in_spec__f__blabla_Type.

A bit weird: giving the closure to a function directly does not triggers the error:

fn takes_closure<F: Fn(&i32) -> i32>(f: F) {}

pub fn f() {
    takes_closure(|&x: &i32| x);
}
arnaudgolfouse commented 1 day ago

Ah, this is not only for patterns, it also happens here:

pub fn f() {
    let clos = #[ensures(result == x.1)]
    |x: &(i32, i32)| x.1;
}