Skip to content

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
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