Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Enable isolating all return statements #5917

Merged
merged 6 commits into from
Nov 15, 2024

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Nov 14, 2024

Description

  • When using {:isolate_assertions}, a separate VC will be generated per pair of return statement and ensure clause.

How has this been tested?

  • Updated the CLI test isolateAllAssertions.dfy

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

@keyboardDrummer keyboardDrummer marked this pull request as ready for review November 15, 2024 14:51
@keyboardDrummer keyboardDrummer requested review from robin-aws and removed request for robin-aws November 15, 2024 15:19
@keyboardDrummer keyboardDrummer enabled auto-merge (squash) November 15, 2024 15:19
Copy link
Member

@robin-aws robin-aws left a comment

Choose a reason for hiding this comment

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

🚀

Verified 2/2 of Foo: assertion at line 10 - verified successfully <redacted>
Verified 1/6 of Foo: assertion at line 10 - verified successfully <redacted>
Verified 2/6 of Foo: assertion at line 11 - verified successfully <redacted>
Verified 3/6 of Foo: return at line 15, assertion at line 7 - verified successfully <redacted>
Copy link
Member

Choose a reason for hiding this comment

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

Nice clarity on what's being verified!

@keyboardDrummer keyboardDrummer merged commit f9c8644 into dafny-lang:master Nov 15, 2024
22 checks passed
@keyboardDrummer keyboardDrummer deleted the isolateAllReturns branch November 15, 2024 18:02
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants