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

Incorrect warning about trait method with no body from dafny audit #5821

Open
atomb opened this issue Oct 9, 2024 · 0 comments
Open

Incorrect warning about trait method with no body from dafny audit #5821

atomb opened this issue Oct 9, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@atomb
Copy link
Member

atomb commented Oct 9, 2024

Dafny version

4.8.1+37d3ff75ce2fd72ce38a1eb7403d671cd01681c9

Code to produce this issue

trait T {
    method M(x: int) returns (r: int)
      requires x > 0
      ensures r < 0
}

Command to run and resulting output

$ dafny audit trait.dfy
trait.dfy(2,11): Warning: M: Compiled declaration has no body and has an ensures clause. Possible mitigation: Provide a body or add `{:axiom}`.
Dafny auditor completed with 1 findings

What happened?

Trait methods with no bodies are not, in fact, compiled declarations, and this warning should not be emitted.

The following two conditions need to be updated:

https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/AST/Members/Function.cs#L63-L65

https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/AST/Members/Method.cs#L57-L59

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

Mac

@atomb atomb added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Oct 9, 2024
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

No branches or pull requests

1 participant