Retrieve the result of drop elaboration

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification

https://aeneasverif.github.io/charon/charon_lib/index.html

Apache License 2.0

105 stars 17 forks source link

Retrieve the result of drop elaboration #152

Open sonmarcho opened 7 months ago

Nadrieril commented 7 months ago

For context:

Drop elaboration is well explained in the dev guide;
It is run in the analysis->runtime MIR phase, the results of which are available only in mir_drops_elaborated_and_const_checked and optimized_mir;
We can't run individual passes ourselves because they're not made public (but we could ask rustc devs for that). EDIT: see below.

Nadrieril commented 6 months ago

I discovered the -Z mir-enable-passes=val flag, which allows choosing exactly which mir passes to run! I'll have to experiment to see if we can get drops without other optimizations.

sonmarcho commented 6 months ago

I discovered the -Z mir-enable-passes=val flag, which allows choosing exactly which mir passes to run! I'll have to experiment to see if we can get drops without other optimizations.

This looks very promising!