Extract local mutability

[yannbolliger]

Introduces the possibility to have let mut variables in function bodies and also mut by-value parameters.
This is still safe, because mutable borrow is still forbidden. Hence, all references can still be erased as they are immutable.

Adds most of the features from #92.

[yannbolliger]

A comment for reviewers: maybe look at the first commit separately, because it just (semantically equivalently) refactors some existing stuff to make it more suitable for the feature additions.

[romac]

Can we also add support for old(expr) and snapshot(expr)?

https://github.com/epfl-lara/stainless/blob/95746730e7bbb5a46279f97325ed38f01d083927/core/src/main/scala/stainless/extraction/imperative/Trees.scala#L116-L124

old is documented here: https://epfl-lara.github.io/stainless/imperative.html#annotations-for-imperative-programming
snapshot was introduced in epfl-lara/stainless#491

[yannbolliger]

Split up the negative tests to one single thing that fails.