Skip to content

Conversation

@keyboardDrummer
Copy link
Member

Fixes #6192

What was changed?

Add fix for exception that could occur when using includes and top level members

How has this been tested?

Added test ast/files/defaultModuleAndInclude/root.dfy

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

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) May 2, 2025 10:50
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.

Just a minor release note improvement, otherwise looks good !
Just a note, I don't see any command like //RUN: or diff or expect in the test file. I was wondering if there was an omission or there is another test format that I ignore?

void AddMethod_Top(MethodOrConstructor m, bool isByMethod, bool includeAllMethods) {
if (!includeAllMethods && !InVerificationScope(m) && !referencedMembers.Contains(m)) {
if (!includeAllMethods &&
!m.EnclosingClass.EnclosingModuleDefinition.EnclosingLiteralModuleDecl.ShouldVerify(program.Compilation) &&
Copy link
Member

Choose a reason for hiding this comment

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

I still don't know what InVerificationScope means so this predicate looks more meaningful.

@@ -0,0 +1 @@
Add fix for exception that could occur when using includes and top level members No newline at end of file
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
Add fix for exception that could occur when using includes and top level members
One less exception when using includes and top level members

Otherwise this will be rendered in the release notes as
"Fix: Add fix for exception that could occur when using includes and top level members"

@keyboardDrummer keyboardDrummer force-pushed the includeAndTopLevelMembers branch from 8b346a8 to 2642035 Compare July 11, 2025 09:48
@keyboardDrummer keyboardDrummer merged commit 220fdec into dafny-lang:master Jul 11, 2025
23 of 24 checks passed
@keyboardDrummer keyboardDrummer deleted the includeAndTopLevelMembers branch July 11, 2025 20:56
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.

Internal Error - Call to Undeclared Procedure

2 participants