gcc/testsuite/gnat.dg/spark2.adb

   1 --  { dg-do compile }
   2
   3 package body SPARK2 with SPARK_Mode is
   4    function Factorial (N : Natural) return Natural is
   5    begin
   6       if N = 0 then
   7          return 1;
   8       else
   9          return N * Factorial (N - 1);
  10       end if;
  11    end Factorial;
  12 end SPARK2;