Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Crash on duplicate declaration errors between a .dfy and a .doo file #4070

Closed
davidcok opened this issue May 23, 2023 · 0 comments · Fixed by #5360
Closed

Crash on duplicate declaration errors between a .dfy and a .doo file #4070

davidcok opened this issue May 23, 2023 · 0 comments · Fixed by #5360
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@davidcok
Copy link
Collaborator

Dafny version

4.1.0+dev

Code to produce this issue

Test4.dfy:

const c := 42

Command to run and resulting output

// RUN: %baredafny build -t:lib "%s" --output "%S/test" > "%t"
// RUN: %baredafny resolve "%s"  "%S/test.doo" >> "%t"

The second command runs resolve on a file and a .doo of itself. It crashes on attempting to put out a 'duplicate declaration' error because the token (at least the filename in the token) associated with the duplicate in the .doo file is not what is expected.

The test Test/doofiles/Test4.dfy contains this problem (currently marked as XFAIL)

What happened?

Crashed instead of putting out error message

What type of operating system are you experiencing the problem on?

Mac
@davidcok davidcok added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 23, 2023
@davidcok davidcok mentioned this issue May 23, 2023
Merged
@keyboardDrummer keyboardDrummer added the crash Dafny crashes on this input, or generates malformed code that can not be executed label Dec 18, 2023
@keyboardDrummer keyboardDrummer added the during 2: compilation of correct program Dafny rejects a valid program during compilation label Feb 7, 2024
@keyboardDrummer keyboardDrummer mentioned this issue Apr 25, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Turning on doofiles/Test4.dfy keyboardDrummer/dafny
2 participants
@keyboardDrummer @davidcok