diff --git a/stainless_extraction/src/expr/block.rs b/stainless_extraction/src/expr/block.rs index 59561295..ea0caec3 100644 --- a/stainless_extraction/src/expr/block.rs +++ b/stainless_extraction/src/expr/block.rs @@ -124,8 +124,12 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> { let exprs = acc_exprs.clone(); acc_exprs.clear(); let body_expr = self.extract_block_(stmts, acc_exprs, acc_specs, final_expr); + // wrap that body expression into the Let - let init = self.extract_expr(init); + + // This is safe, because we don't support mutable references. + let init = self.extract_aliasable_expr(init); + let last_expr = if vd.is_mutable() { f.LetVar(vd, init, body_expr).into() } else { diff --git a/stainless_frontend/tests/pass/mut_local_lets.rs b/stainless_frontend/tests/pass/mut_local_lets.rs index 46d58f6a..41f10998 100644 --- a/stainless_frontend/tests/pass/mut_local_lets.rs +++ b/stainless_frontend/tests/pass/mut_local_lets.rs @@ -2,9 +2,22 @@ extern crate stainless; -pub enum IntOption { - None, - Some(i32), +pub fn f(option: Option) { + // Again, local mutation + let mut option2 = None; + let mut option = None; + option2 = option; + option = Some(123); +} + +pub struct Thing { + field: T, +} + +pub fn change_thing(thing: Thing, t: T) -> Thing { + let mut new_field = thing.field; + new_field = t; + Thing { field: new_field } } pub fn main() { @@ -13,11 +26,4 @@ pub fn main() { assert!(x == 1); x = 3; assert!(x == 3); - - // Again, local mutation - let option = IntOption::Some(2); - let mut option2 = IntOption::None; - let mut option = IntOption::None; - option2 = option; - option = IntOption::Some(123); }