diff --git a/stainless_extraction/src/expr/field.rs b/stainless_extraction/src/expr/field.rs index 8e75368f..50ec74b8 100644 --- a/stainless_extraction/src/expr/field.rs +++ b/stainless_extraction/src/expr/field.rs @@ -36,6 +36,15 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> { ) .into() } + TyKind::Tuple(substs) => { + let lhs = self.extract_expr(lhs); + f.FieldAssignment( + self.synth().tuple_select(substs.len(), lhs, name.index()), + self.synth().mut_cell_value_id(), + value, + ) + .into() + } ref t => self.unsupported_expr( lhs.span, format!("Cannot extract assignment to type {:?}", t), diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs index 7ed18508..248bf11c 100644 --- a/stainless_frontend/tests/extraction_tests.rs +++ b/stainless_frontend/tests/extraction_tests.rs @@ -138,6 +138,7 @@ define_tests!( pass: mut_ref_immut_borrow, pass: mut_ref_tuple, pass: mut_return, + pass: mut_tuple, pass: nested_spec, pass: nested_spec_impl, pass: panic_type, diff --git a/stainless_frontend/tests/pass/mut_tuple.rs b/stainless_frontend/tests/pass/mut_tuple.rs new file mode 100644 index 00000000..ceb2ef41 --- /dev/null +++ b/stainless_frontend/tests/pass/mut_tuple.rs @@ -0,0 +1,8 @@ +extern crate stainless; + +pub fn main() { + let mut x = (123, false); + let y = x; + x.1 = true; + assert!(!y.1 && x.1) +}