search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

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

Open atomb opened 1 month ago

atomb commented 1 month ago

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