-
Notifications
You must be signed in to change notification settings - Fork 261
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
Error in function-by-method verification: Type parameter could not be determined #4998
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Comments
alex-chew
added
the
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
label
Jan 19, 2024
alex-chew
changed the title
Type parameter
Error in function-by-method verification: Type parameter could not be determined
Jan 19, 2024
RustanLeino
added a commit
that referenced
this issue
Feb 8, 2024
…ion (#5068) This PR fills in any type arguments `X` to the `result = F<X>(args)` postcondition that's generated for the method part of a `function-by-method` declaration. Fixes #4998 Reviewer notes: The desugaring of `function-by-method` is done in two places in the code. I filled in the type arguments in both places. However, in the second place (which is for `{:test}` functions/methods), `dafny` would crash if any type parameters were declared (even for type parameters that were not auto-init `(0)`). Since the `{:test}` was already not allowed for functions/methods with parameters, I also added error messages if `{:test}` is used with a function/method with type parameters. <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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Dafny version
4.2.0, 4.3.0, 4.4.0
Code to produce this issue
Command to run and resulting output
What happened?
It seems that the snippet should verify, but it doesn't. Writing either the predicate by itself, or the method by itself, works as expected.
This behavior occurs in 4.2.0, 4.3.0, and 4.4.0.
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: