with Ada.Unchecked_Deallocation;

package body Spark_Unbound.Safe_Alloc with SPARK_Mode is

   package body Definite with SPARK_Mode is
      
      function Alloc return T_Acc is
         pragma SPARK_Mode (Off); -- Spark OFF for exception handling
      begin
         return new T;
      exception
         when Storage_Error =>
            return null;
      end Alloc;

      procedure Free (Pointer : in out T_Acc) is
         procedure Dealloc is new Ada.Unchecked_Deallocation (T, T_Acc);
      begin
         Dealloc (Pointer);
      end Free;
   end Definite;
   
   package body Arrays with SPARK_Mode is

      function Alloc (First, Last : Index_Type) return Array_Type_Acc is
         pragma SPARK_Mode (Off); -- Spark OFF for exception handling
      begin
         return new Array_Type(First .. Last);
      exception
         when Storage_Error =>
            return null;
      end Alloc;
      
      procedure Free (Pointer : in out Array_Type_Acc) is
         procedure Dealloc is new Ada.Unchecked_Deallocation (Array_Type, Array_Type_Acc);
      begin
         Dealloc (Pointer);
      end Free;
      
   end Arrays;
   
end Spark_Unbound.Safe_Alloc;