diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs index d98e2d44..5d97fdb9 100644 --- a/stainless_frontend/tests/extraction_tests.rs +++ b/stainless_frontend/tests/extraction_tests.rs @@ -130,6 +130,7 @@ define_tests!( pass: mut_ref_borrow_6, pass: mut_ref_borrow_7, pass: mut_ref_borrow_8, + pass: mut_ref_borrow_9, pass: mut_ref_immut_borrow, pass: mut_return, pass: nested_spec, diff --git a/stainless_frontend/tests/pass/mut_ref_borrow_9.rs b/stainless_frontend/tests/pass/mut_ref_borrow_9.rs new file mode 100644 index 00000000..b460c1b0 --- /dev/null +++ b/stainless_frontend/tests/pass/mut_ref_borrow_9.rs @@ -0,0 +1,43 @@ +extern crate stainless; + +struct S(T); +struct Container { + s: S, +} + +pub fn main() { + let mut c = Container { s: S("hello") }; + + match &mut c.s { + S(v) if *v == "hello" => *v = "world", + _ => {} + }; + + assert!(c.s.0 == "world") +} + +/* + +Desired Scala translation: + +import stainless.annotation._ + +object Fields { + case class S[@mutable T](_0: MutCell[T]) + case class MutCell[@mutable T](var value: T) + case class Container[@mutable T](s: MutCell[S[T]]) + + def main: Unit = { + var c: Container[String] = Container(MutCell(S(MutCell("hello")))) + + (c.s match { + case MutCell(S(v)) if v.value == "hello" => + v.value = "world" + case _ => + () + }) + assert(c.s.value._0.value == "world") + } +} + + */