Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3
  • why3why3
  • Issues
  • #394

Closed
Open
Opened Oct 16, 2019 by DAILLER Sylvain@sdaillerDeveloper

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#394