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.

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

--show-snippets does not work for parse errors #3304

Closed
davidcok opened this issue Dec 31, 2022 · 0 comments · Fixed by #4064
Closed

--show-snippets does not work for parse errors #3304

davidcok opened this issue Dec 31, 2022 · 0 comments · Fixed by #4064
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line part: parser First phase of Dafny's pipeline

Comments

@davidcok
Copy link
Collaborator

davidcok commented Dec 31, 2022

Dafny version

3.10.0+dev

Code to produce this issue

const c = 5

Command to run and resulting output

dafny verify --show-snippets test.dfy

What happened?

Got:
/Users/davidcok/projects/dafny/dafny/Test/tmp.dfy(1,10): Error: a const field should be initialized using ':=', not '='
1 parse errors detected in /Users/davidcok/projects/dafny/dafny/Test/tmp.dfy

Expected to see a display of source code, like this for verification errors:
|
3 | assert false;
| ^^^^^

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 Dec 31, 2022
@MikaelMayer MikaelMayer added part: CLI interacting with Dafny on the command line part: parser First phase of Dafny's pipeline labels Jan 4, 2023
@davidcok davidcok self-assigned this Apr 22, 2023
davidcok added a commit that referenced this issue May 31, 2023
Fixes #3304

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: davidcok <davidcok@github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line part: parser First phase of Dafny's pipeline
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants