GitLab

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