Verification of size aspects with Message'Last

[jklmnn]

I checked the flexibility of the shortcut syntax for size aspects and noticed that it is possible to create messages with overlapping fields:

package P1 is

   type Kind is mod 2**16;

   type Frame is
      message
         Kind : Kind
            then Payload
                if Kind = 1
            then Kind2
                if Kind = 2;
         Kind2 : Kind;
         Payload : Opaque
            with Size => Message'Last - Kind'Last;
      end message;

end P1;

In this case Payload always ranges from Kind to the end of the message. If Kind = 2 then Kind2 will be overwritten by payload. This spec is not rejected.

[treiher]

That is not related to the shortcut syntax. The semantically equivalent specification is also accepted:

package Test is

   type Kind is mod 2**16;

   type Frame is
      message
         Kind : Kind
            then Payload
               with Size => Message'Last - Kind'Last
               if Kind = 1
            then Kind2
               if Kind = 2;
         Kind2 : Kind
            then Payload
               with Size => Message'Last - Kind'Last;
         Payload : Opaque;
      end message;

end Test;

[treiher]

This specification should also not be accepted:

package Test is

   type Kind is mod 2**16;

   type Frame is
      message
         Kind : Kind
            then Payload
               with Size => Message'Last - Kind'Last
               if Kind = 1
            then Kind2
               if Kind = 2;
         Kind2 : Kind
            then Payload
               with Size => Message'Last + 128;
         Payload : Opaque;
      end message;

end Test;

[senier]

This will be obsolete once #736 is implemented.