Preconditions don't work with GNAT?

Question

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.

Answer 1

You need to enable assertions by compiling with -gnata:

$ gnatmake -gnat12 -gnata test.adb
gcc -c -gnat12 -gnata test.adb
gnatbind -x test.ali
gnatlink test.ali
gnatlink: warning: executable name "test" may conflict with shell command

$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A =  987
B =  987

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from test.adb:13 instantiated at test.adb:39

Pragma Assertion_Policy isn't implemented in FSF GNAT <= 4.8 (well, you can't use it to turn checks on or off). However, it is implemented in GNAT GPL 2013; if you're not using GNAT Project files, this would mean creating a file gnat.adc containing

pragma Assertion_Policy (Check);

Minor point: 'Size is in bits, not bytes, so Storage_Count isn't really the right type for it!