Support for local imperative features - Githubissues

epfl-lara / rust-stainless

An experimental Rust frontend for Stainless

Apache License 2.0

6 stars 2 forks source link

Support for local imperative features #92

Open romac opened 3 years ago

romac commented 3 years ago

Add support for local mutation (ie. no mutable references, just mutable variables/parameters within a function).

[x] Blocks - { a; b; c } (Block)
[x] Declare variables - let mut x: i32 = 0; body (LetVar)
[x] Assignments - vd = value (Assignment)
[x] Field assignment - expr.field = value (FieldAssigment)
[x] ~Return statement - return expr (Return)~ => tracked here #71
[ ] Old - old(expr) (Old)
[ ] Snapshot - snapshot(expr) (Snapshot)

Start thinking about:

[ ] Mutable maps
[ ] Arrays

yannbolliger commented 3 years ago

The big question here, is what we want to do with references. For now, we allowed references because we knew that mutability was prohibited. As soon as mutability comes back, we need to revise, how we deal with references.

EDIT: question answered here in #98.