search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.27k stars 94 forks source link

Dynamic and Ref(Dynamic) codegen to same fat pointer #82

Closed markrtuttle closed 2 years ago

markrtuttle commented 3 years ago

The method codegen_ty produces the same fat pointer for both the Dynamic and Ref(Dyanmic) mir type kinds. I'm not sure what Dynamic should codegen since a trait object can only be accessed via a pointer (a fat pointer). But probably no one should be trying to codegen Dynamic itself, and we should panic if anyone tries to do so.

avanhatt commented 3 years ago

In some cases where closures or function pointers are passed as arguments; it seems like we are codegening just a Dynamic.

avanhatt commented 3 years ago

Possibly related: https://github.com/model-checking/rmc/issues/95

danielsn commented 2 years ago

Appears to be related to projection issue