search

epfl-lara / rust-stainless

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

Debug field mutability #150

Closed yannbolliger closed 3 years ago

yannbolliger commented 3 years ago

Currently it is possible to have a struct that has no mutability annotation (#[var(b)]):

struct A {
  a: i32,
  b: bool
}

Then take such a struct as mut param in a function:

fn f(mut a: A) {
  a.b = false;
}

This is allowed but very dangerous because AntiAliasing in Scala Stainless will simply and silently erase the field assignments to non-var fields with Unit. This is fixed by https://github.com/epfl-lara/stainless/pull/1016.