Re: A hole in Ada type safety

[AdaMagica <christ-usch.grein@t-online.de>]

Randy has already given the answer.

Let me add a further remark (but note, I'm no language lawyer):

You argue about the return statement. But there is no return statement
involved in the RM with Unchecked_Conversion, it's just compiler magic
that is being performed. (Being intrinsic, Unchecked_Conversion need
not be implemented in Ada. In fact, I think there is no code at all,
it just takes the bit pattern as is and reinterpretes it.)

Run the following test program:

package UC is

  type LP1 is limited private;

  procedure Set (X: out LP1; to: Integer);

  type LP2 is limited private;

private

  type LP1 is limited record
    I: Integer := 1234;
  end record;

  type LP2 is limited record
    I: Integer := Integer'First;
  end record;

end UC;
package body UC is

  procedure Set (X: out LP1; to: Integer) is
  begin
    X.I := to;
  end Set;

end UC;
with Ada.Text_IO;
with Ada.Unchecked_Conversion;
with UC;

procedure Test_UC is

  function LP1_LP2 is new Ada.Unchecked_Conversion (UC.LP1, UC.LP2);
  function LP2_I   is new Ada.Unchecked_Conversion (UC.LP2, Integer);

  X: UC.LP1;
  Y: constant UC.LP2    :=   LP1_LP2 (X);  -- new object built in
place
  Z:          UC.LP2 renames LP1_LP2 (X);  -- read-only view

begin
 
-- expected result
  Ada.Text_IO.Put_Line (Integer'Image (LP2_I (Y)) & Integer'Image
(LP2_I (Z)));  -- 1234 1234
  UC.Set (X, -100);
  Ada.Text_IO.Put_Line (Integer'Image (LP2_I (Y)) & Integer'Image
(LP2_I (Z)));  -- 1234-100

end Test_UC;