Internal constant fields (internal const): They have the same type and assigned and read using regular field read and field update.
Mutable fields (var): They are wrapped with ::dafny_runtime::Field<...> to avoid any soundness issue, and use the wrappers read_field and modify_field to read and modify them.
Constant fields (const): They are called with a function call with zero argument.
Before this PR, only the last two were implemented, which lead to issues when trying to assign the default value of a class constant.
This issue was not captured because the test started to fail but since it's was marked %testForEachCompiler and these tests are ignored in the CI, we did not detect it.
How has this been tested?
Updated the file classes.dfy. All other tests in comp/rust should pass.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Fixes #5833
Description
There are now three kinds of generated fields:
::dafny_runtime::Field<...>to avoid any soundness issue, and use the wrappersread_fieldandmodify_fieldto read and modify them.Before this PR, only the last two were implemented, which lead to issues when trying to assign the default value of a class constant. This issue was not captured because the test started to fail but since it's was marked
%testForEachCompilerand these tests are ignored in the CI, we did not detect it.How has this been tested?
Updated the file classes.dfy. All other tests in comp/rust should pass.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.