Fix anti-aliasing problems by using fresh copy

epfl-lara / rust-stainless

An experimental Rust frontend for Stainless

Apache License 2.0

6 stars 2 forks source link

Fix anti-aliasing problems by using fresh copy #156

Closed yannbolliger closed 3 years ago

yannbolliger commented 3 years ago

Closes #154.

By using the new Stainless primitive, it is possible to translate consumed/owned by-value parameters in Rust into fresh copies in Stainless which don't incur aliasing restrictions.

Add regenerated AST trees.
Add test case.
Use fresh copy for mutable by-value parameters.