Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Bad translation of ensures with &mut

I'm having a hard time reproducing (see https://hax-playground.cryspen.com/#fstar/2a17a0beef/gist=8689d6b1b90ffbdfde130b3fe5710901). But, re-extracting with this commit I get indeed this bug, I think that might be a interface-only bug

Bad translation of ensures with &mut

@karthikbhargavan, I think this was due to a stale hax-lib actually! I spent a lot of time looking at it, and at the end I think it's only a version...

Prefer using `rustc_middle::ty` types over `rustc_hir` ones

Still relevant

Prefer using `rustc_middle::ty` types over `rustc_hir` ones

We won't implement that, instead we'll switch to FullDef in our Rust engine, and drop the OCaml one along with those HIR types

Double return bug

Thanks for the bug report Mamone! I'm looking at it now, here is a minimized reproducer: ```rust fn f(n: &mut usize) { for _ in 0..10 { *n += 1;...

Double return bug

Thanks for the issue! I spent a few hours on that, I don't have a fix yet. I think this issue shows up mainly in functions that ends with a...

Double return bug

I removed the due date and set the priority to low. We have a workaround, and loads of other things to do, so let's pick that whenever we have time.

Double return bug

My reproducer: ```rust fn f(n: &mut usize) { for _ in 0..10 { *n += 1; } } ``` works now, let's find another reproducer or close otherwise

Double return bug

Well, we did no any work towards this 😅 Somehow something fixed it. I think that's one of the new phases added by @maximebuyse that interact with this. Shall we...

fix(engine/importer): use correct field to import concrete implexprs

Hi, thanks for your PR! Sorry for the delay, the week is quite busy... will try to look into those tests tomorrow!