Re: GNAT proposal: note on implicit exceptions insertion

[Brad Moore <bmoore.ada@gmail.com>]

One option would be to write the code you want checked in SPARK.

For example, from your example above, one could write....
 
package P with SPARK_Mode is

   subtype Index_Type is Integer range 1 .. 100;
   
   My_Array : array (Index_Type) of Boolean;
   
   procedure Foo (Index : Integer);

end P;

package body P with SPARK_Mode is

   procedure Foo (Index : Integer) is
   begin
      My_Array (Index) := True;  --  SPARK detects exception may be raised here
   end Foo;

end P;


The code compiles in Ada, but the SPARK prover complains....

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
p.adb:6:17: medium: array index check might fail (e.g. when Index = 0)

Brad