Mentions légales du service

Skip to content
Snippets Groups Projects
Open Warning on useless exception catching
  • View options
  • Warning on useless exception catching

  • View options
  • Open Issue created by DAILLER Sylvain

    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
    • Merge request
    • Branch

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading