Skip to content

Conversation

RustanLeino
Copy link
Collaborator

This PR fixes a soundness issue where, previously, type properties of this were assumed already in the first phase of constructors. Now they are assumed at the time of the new;.

Fixes #5136

Description

The details of the fix are as described in issue #5136.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@RustanLeino RustanLeino enabled auto-merge (squash) October 30, 2024 20:27
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've tested the test that reproduces the soundness issue, and the expect file demonstrates that this PR fixes the soundness issue. The where clause was indeed responsible for setting a constraint too early on the return variable, and removing it and putting it as an assumption in the "new;" seems the right thing to do

@RustanLeino RustanLeino merged commit 7e637e6 into dafny-lang:master Oct 30, 2024
22 checks passed
@RustanLeino RustanLeino deleted the issue-5136 branch October 30, 2024 22:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Empty type initialization leads to proving false
2 participants