Warning on useless exception catching
This is a feature request and I don't know if it would easily be doable (it seems to be possible as the converse is notified to the user: exceptions that are raised but not caught must appear in the raises
contract).
In the following, I would like a warning on the last line telling me that TODO
is caught but never raised:
use int.Int
use ref.Ref
exception TODO
exception TODO2
let f (a: ref int)
ensures { !a = 3 }
=
try raise TODO2 with
| TODO2 -> a := 3
| TODO -> a := 4 end