diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs index 1c99ae0c..df9dd7db 100644 --- a/stainless_frontend/tests/extraction_tests.rs +++ b/stainless_frontend/tests/extraction_tests.rs @@ -91,6 +91,7 @@ define_tests!( pass: let_type, pass: list_binary_search, pass: monoid, + pass: mut_local_fields, pass: mut_local_lets, pass: mut_local_params, pass: mut_ref_immut_borrow, diff --git a/stainless_frontend/tests/pass/mut_local_fields.rs b/stainless_frontend/tests/pass/mut_local_fields.rs new file mode 100644 index 00000000..ce00c647 --- /dev/null +++ b/stainless_frontend/tests/pass/mut_local_fields.rs @@ -0,0 +1,15 @@ +extern crate stainless; +use stainless::*; + +#[var(field)] +struct S { + field: i32, +} + +pub fn main() { + // field assignment + let mut s = S { field: 123 }; + assert!(s.field == 123); + s.field = 456; + assert!(s.field == 456); +} diff --git a/stainless_frontend/tests/pass/mut_local_lets.rs b/stainless_frontend/tests/pass/mut_local_lets.rs index 1784917f..46d58f6a 100644 --- a/stainless_frontend/tests/pass/mut_local_lets.rs +++ b/stainless_frontend/tests/pass/mut_local_lets.rs @@ -7,10 +7,6 @@ pub enum IntOption { Some(i32), } -struct S { - field: i32, -} - pub fn main() { // Local mutation is ok. let mut x = 1; @@ -24,10 +20,4 @@ pub fn main() { let mut option = IntOption::None; option2 = option; option = IntOption::Some(123); - - // field assignment - let mut s = S { field: 123 }; - assert!(s.field == 123); - s.field = 456; - assert!(s.field == 456); }