Warning on pure functions not using result
Hello,
This is a feature request. I think it could be useful to have a warning when some Why3 pure function has an ensures
but do not use the result
keyword. An example of this is the following:
use int.Int
val eq (x: int) (y : int) : bool
ensures { x = y}
In this example, the intended code was:
val eq (x: int) (y : int) : bool
ensures { result = (x = y)}
I think this kind of mistake can be detected automatically (and is almost always an error, am I mistaken ?):
- function does not has side effect
- and ensures does not use
result