with Ada.Unchecked_Conversion;
with Interfaces; use Interfaces;
with System;     use System;

package UC_To_Access with SPARK_Mode => On is
   type Int_Access is access all Integer;

   function Uns_To_Int_Access is new Ada.Unchecked_Conversion (Unsigned_64, Int_Access);
   --  Accepted with warnings
   function Uns_From_Int_Access is new Ada.Unchecked_Conversion (Int_Access, Unsigned_64);
   --  Rejected

   C1 : constant Int_Access := Uns_To_Int_Access (30);

   function Addr_To_Int_Access is new Ada.Unchecked_Conversion (Address, Int_Access);
   --  Accepted with warnings
   function Addr_From_Int_Access is new Ada.Unchecked_Conversion (Int_Access, Address);
   --  Rejected

   Addr : Address with Import;
   C2 : constant Int_Access := Addr_To_Int_Access (Addr);

   type PS_Access is access Integer;

   function Uns_To_PS_Access is new Ada.Unchecked_Conversion (Unsigned_64, PS_Access);
   --  Rejected
end UC_To_Access;