Ensure exception coverage at compile time

Question

Is there a way to get GNAT to ensure all exception cases are handled?

To give an example:

   package IO renames Ada.Text_IO;
   package EIO renames Ada.IO_Exceptions;

   procedure Open_File (File : in out IO.File_Type) is
   begin
      IO.Open (File, IO.In_File, "example.txt");
   exception
      when EIO.Use_Error =>
         IO.Put_Line ("Use!");
      when EIO.Device_Error =>
         IO.Put_Line ("Device!");
   end Open_File;

Open can also raise Name_Error so I would like GNAT to warn that case has not been handled.

I found pragma Restrictions (No_Exception_Propagation) but that seems to apply the check to the standard library calls as well so Open becomes unusable because it propagates exceptions itself. If I apply this to my example, I get:

14:07: warning: pragma Restrictions (No_Exception_Propagation) in effect
14:07: warning: this handler can never be entered, and has been removed
16:07: warning: pragma Restrictions (No_Exception_Propagation) in effect
16:07: warning: this handler can never be entered, and has been removed

For an example of what I want from another language; Nim has a raises pragma to annotate what exceptions a procedure can raise, which the compiler enforces. The list can be empty, ie. raises: [], and the compiler will require that all exceptions will be handled and not propagate. Is there an equivalent to this in Ada?

Using SPARK, you can guarantee all exceptions are handled in SPARK-verified sections of your program, by proving that none will ever be raised... — user_1818839

thindil thindil · Accepted Answer · 2020-09-09T08:01:36

If you want to handle all available exceptions, you can use when others in exception section. Your example will look that:

package IO renames Ada.Text_IO;
package EIO renames Ada.IO_Exceptions;

procedure Open_File (File : in out IO.File_Type) is
begin
   IO.Open (File, IO.In_File, "example.txt");
exception
   when An_Exception : others =>
      IO.Put_Line (EIO.Exception_Message(An_Exception));
end Open_File;

If you want to handle each exception in a separated way, then you have to list each of exceptions separately (as in your example). But compiler will not warn you about missing handler of an exception.

Ensure exception coverage at compile time

2 Answers