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

Passing a DLL path that doesn't exist raises an exception #2719

Closed
robin-aws opened this issue Sep 9, 2022 · 0 comments · Fixed by #3331
Closed

Passing a DLL path that doesn't exist raises an exception #2719

robin-aws opened this issue Sep 9, 2022 · 0 comments · Fixed by #3331
Assignees
@robin-aws
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line

Comments

@robin-aws
Copy link
Member

robin-aws commented Sep 9, 2022 •
edited by MikaelMayer
Loading

dafny foobar.dfy gives you a relatively clean Unable to open included file error, but dafny foobar.dll leads to a FileNotFoundException (because it tries to extract the DafnySourceAttribute text if it exists, without handling this case).

method Test() {}
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label crash Dafny crashes on this input, or generates malformed code that can not be executed part: CLI interacting with Dafny on the command line labels Sep 9, 2022
@robin-aws robin-aws self-assigned this Sep 9, 2022
@robin-aws robin-aws mentioned this issue Sep 9, 2022
Merged
MikaelMayer added a commit that referenced this issue Jan 5, 2023
@MikaelMayer
Add test for issue #2719
805cc17
@MikaelMayer MikaelMayer mentioned this issue Jan 5, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robin-aws robin-aws

Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Other CLI files that are not found do not trigger exceptions dafny-lang/dafny
1 participant
@robin-aws