Preconditions don't work with GNAT?

Preconditions don't work with GNAT?

I'm still kind of new to Ada and I think I'm misunderstanding the use of
Preconditions, because looking through GNAT RM it seems the checks aren't
performed at runtime. Also, the GNAT RM for Precondition here doesn't
specifiy which exception is thrown if the precondition is not met.
Here is the code I'm trying:
procedure Test is
begin
generic
type Element_Type is private;
use System.Storage_Elements;
procedure Byte_Copy (Destination : out Element_Type;
Source : in Element_Type;
Size : in Storage_Count := Element_Type'Size)
with Pre =>
Size <= Destination'Size and
Size <= Source'Size;
procedure Byte_Copy (Destination : out Element_Type;
Source : in Element_Type;
Size : in Storage_Count := Element_Type'Size)
is
subtype Byte_Array is Storage_Array (1 .. Size / System.Storage_Unit);
Write, Read : Byte_Array;
for Write'Address use Destination'Address;
for Read'Address use Source'Address;
begin
Ada.Text_IO.Put_Line("Size to copy =" & Size'Img &
" and Source'Size =" & Source'Size'Img);
if Size > Destination'Size or else Size > Source'Size then
raise Constraint_Error with
"Source'Size < Size or else > Destination'Size";
end if;
for N in Byte_Array'Range loop
Write (N) := Read (N);
end loop;
end Byte_Copy;
procedure Integer_Copy is new Byte_Copy(Integer);
use type System.Storage_Elements.Storage_Count;
A, B : Integer;
begin
A := 5;
B := 987;
Ada.Text_IO.Put_Line ("A =" & A'Img);
Ada.Text_IO.Put_Line ("B =" & B'Img);
Integer_Copy (A, B, Integer'Size / 2);
Ada.Text_IO.Put_Line ("A = " & A'Img);
Ada.Text_IO.Put_Line ("B = " & B'Img);
Integer_Copy (A, B, Integer'Size * 2);
Ada.Text_IO.Put_Line ("A =" & A'Img);
Ada.Text_IO.Put_Line ("B =" & B'Img);
end Test;
If I understand things correctly, then this programme should raise some
unspecified exception before even calling the Put_Line procedure. But you
can see that when I run the programme, the procedure is called with an
invalid Size argument which violates the Precondition Destination'Size ¡Ý
Size ¡Ü Source'Size. Instead, I have to place an if statement to actually
catch the error and raise the exception Constraint_Error to keep things
sane.
$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A = 987
B = 987
Size to copy = 64 and Source'Size = 32
raised CONSTRAINT_ERROR : Source'Size < Size or else > Destination'Size
I have tried variations like adding pragma Precondition ( ... ) but that
doesn't work either.
One weird thing is that the programme actually compiles if I repeat the
with Pre => clause in the generic procedure body/definition. It normally
doesn't allow this for procedures and raises an error (i.e., Preconditions
should only be in formal declarations, not in the definition). Are generic
procedures an exception in this case?
I'm also surprised that use clause can be added in generic procedure
declarations. This makes defining formal parameter names easier (ones
which are obscenely long) but looks more like a bug because this cannot be
done for normal/regular procedure declarations.
P.S. I wanted to implement my closest possible imitation of memcpy() from
C, in the Ada language for learning purposes.