search

epfl-lara / rust-stainless

An experimental Rust frontend for Stainless
Apache License 2.0
6 stars 2 forks source link

Fix mutable parameters of mutable ADTs #153

Closed yannbolliger closed 3 years ago

yannbolliger commented 3 years ago

Closes #150 but not the anti-aliasing problems described in https://github.com/epfl-lara/rust-stainless/issues/154.

This PR incorporates the fixed version of Stainless that fixes the linked issue. For the anti-aliasing problem of mutable ADTs, an approach of deeply copying the ADT at the start of the function by doing a pattern match and then field-wise copy was tried but abandoned (#155).

yannbolliger commented 3 years ago

Converting to draft, because this will only work generally with deep copies of ADTs.