AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Fix phase ordering problem. #33

Closed msprotz closed 2 months ago

msprotz commented 2 months ago

The remove_unused phase generates left-nested let-bindings, and therefore needs to occur before let_to_sequence and vice-versa, which re-normalizes let-bindings to be right-nesting.

The AstToCStar name management facility expects proper right-nesting, otherwise name collision avoidance does not work.

This fixes #31