diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 55fb008c70c..e8af65fc034 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -3398,9 +3398,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler { rhs]); newEnv := newEnv.RemoveAssigned(isAssignedVar); } else { - error := Some("Unespected field to assign whose isAssignedVar is not in the environment: " + isAssignedVar); - generated := - R.AssignMember(R.RawExpr(error.value), fieldName, rhs); + // Already assigned, safe to override + generated := R.Assign(Some(R.SelectMember(modify_macro.Apply1(thisInConstructor), fieldName)), rhs); } case _ => if onExpr != R.Identifier("self") { diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index afc7e6a72ea..b79687f60c2 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -2855,8 +2855,7 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, DCOMP._ISelfInfo generated = (((RAST.__default.dafny__runtime).MSel((this).update__field__uninit__macro)).AsExpr()).Apply(Dafny.Sequence.FromElements((this).thisInConstructor, RAST.Expr.create_Identifier(_4_fieldName), RAST.Expr.create_Identifier(_8_isAssignedVar), rhs)); newEnv = (newEnv).RemoveAssigned(_8_isAssignedVar); } else { - (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Unespected field to assign whose isAssignedVar is not in the environment: "), _8_isAssignedVar)); - generated = RAST.__default.AssignMember(RAST.Expr.create_RawExpr((this.error).dtor_value), _4_fieldName, rhs); + generated = RAST.Expr.create_Assign(Std.Wrappers.Option.create_Some(RAST.AssignLhs.create_SelectMember(((this).modify__macro).Apply1((this).thisInConstructor), _4_fieldName)), rhs); } goto after_match1; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy new file mode 100644 index 00000000000..55b40c2bbab --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy @@ -0,0 +1,14 @@ +// RUN: %testDafnyForEachCompiler "%s" + +class Cl { + const c: bool + constructor(c: bool) { + this.c := c; + this.c := c; + } +} + +method Main() { + var cl := new Cl(false); + print cl.c, "\n"; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect new file mode 100644 index 00000000000..c508d5366f7 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5642.dfy.expect @@ -0,0 +1 @@ +false diff --git a/docs/dev/news/5642.fix b/docs/dev/news/5642.fix new file mode 100644 index 00000000000..b8dbeb1f2af --- /dev/null +++ b/docs/dev/news/5642.fix @@ -0,0 +1 @@ +Support for double constant initialization in Dafny-to-Rust \ No newline at end of file