Nadrieril

There's been [attempts](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/.60box_new.60.20as.20a.20macro.3F/with/546307696) to get rid of this weird behavior on the rustc side, this might end up fixing itself :D

Hi! Yep, this is an artefact of us using an early version of MIR. We absolutely would like correct drops, see #152. We're working on it, it's a current priority.

It's indeed pretty much resolved by `--mir elaborated`, but I'd like to make that the default before closing the issue

I'm glad `--mir elaborated` is working well for you!

It's be exactly the same drops as rustc, since it's rustc who gives them to us. One limitation is #684 which is tracked separately. I'm not aware of any bugs...

```rust thread_local!(static FOO: u32 = 42); ``` actually expands to ```rust const FOO: ::std::thread::LocalKey = { #[inline] fn __rust_std_internal_init_fn() -> u32 { 42 } unsafe { ::std::thread::LocalKey::new(const { if ::std::mem::needs_drop::()...

We'll have to do more deduplication, in particular for passes that traverse a type.

Actually the first step would be to hash-cons `TraitRef`s in both hax and charon so we can piggy-back on rustc's interning to only translate each ref once. Second step would...

In principle that's not hard, I can iterate over all the loaded crates. That would be a natural extension of https://github.com/AeneasVerif/charon/issues/336. What's your usecase?

> In principle, something similar to Kani really. I don't actually know what Kani does here, doesn't Kani use monomorphized code? > One of the analyses we want to try...