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

Missing docstring in predicate #3840

Closed
davidcok opened this issue Apr 4, 2023 · 0 comments · Fixed by #3847
Closed

Missing docstring in predicate #3840

davidcok opened this issue Apr 4, 2023 · 0 comments · Fixed by #3847
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@davidcok
Copy link
Collaborator

davidcok commented Apr 4, 2023

Dafny version

4.0.0+dev

Code to produce this issue

predicate p()
    // Always true. Every time.
    ensures p() == true
  { true }

Command to run and resulting output

In the AST the above predicate does not have a docstring.
Equivalent code with a /** */ comment does not have a docstring.
Equivalent code for a function is OK.
Equivalent code without a specification is OK.

What happened?

No docstring in the AST.

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 Apr 4, 2023
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
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants