Skip to content

Enable isolating all return statements#5917

Merged
keyboardDrummer merged 6 commits into
dafny-lang:masterfrom
keyboardDrummer:isolateAllReturns
Nov 15, 2024
Merged

Enable isolating all return statements#5917
keyboardDrummer merged 6 commits into
dafny-lang:masterfrom
keyboardDrummer:isolateAllReturns

Conversation

@keyboardDrummer

@keyboardDrummer keyboardDrummer commented Nov 14, 2024

Copy link
Copy Markdown
Member

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

@robin-aws robin-aws left a comment

Copy link
Copy Markdown
Member

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
Copy Markdown
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
@keyboardDrummer keyboardDrummer deleted the isolateAllReturns branch November 15, 2024 18:02
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.

2 participants