Refinement using parameterized message generates invalid code

[jklmnn]

Using a parameterized message as follows:

package Test is

   type Length is range 0 .. 2 ** 24 - 1 with Size => 32;

   type Frame is
      message
         Length : Length;
         Payload : Opaque
            with Size => Length * 8;
      end message;

   type Packet (Length : Length) is
      message
         Payload : Opaque
            with Size => Length * 8;
      end message;

   for Test::Frame use (Payload => Test::Packet);

end Test;

generates code that fails to compile with the following error:

Setup
   [mkdir]        object directory for project Out_Project
Compile
   [Ada]          rflx-rflx_builtin_types-conversions.ads
   [Ada]          rflx-rflx_types.ads
   [Ada]          rflx-rflx_arithmetic.adb
   [Ada]          rflx-rflx_scalar_sequence.adb
   [Ada]          rflx-rflx_generic_types.adb
   [Ada]          rflx.ads
   [Ada]          rflx-test-packet.adb
   [Ada]          rflx-test-contains.adb
rflx-test-contains.adb:23:23: error: no candidate interpretations match the actuals:
rflx-test-contains.adb:23:23: error: missing argument for parameter "Length" in call to "INITIALIZE" declared at rflx-test-packet.ads:87
rflx-test-contains.adb:23:23: error: too many arguments in call to "RFLX.Test.Packet.Initialize"
rflx-test-contains.adb:36:23: error: no candidate interpretations match the actuals:
rflx-test-contains.adb:36:23: error: missing argument for parameter "Length" in call to "INITIALIZE" declared at rflx-test-packet.ads:87
rflx-test-contains.adb:36:23: error: too many arguments in call to "RFLX.Test.Packet.Initialize"
gprbuild: *** compilation phase failed

[senier]

IMHO this should be rejected altogether. I guess we'll need a way to associate the parameter with a field of the outer message (or something completely different).

[treiher]

I agree that the given refinement is not suitable and should be rejected. It must be enforced that all parameters of an inner messages are defined using an expression (which could refer to fields of the outer message). For the given example, a valid refinement could be specified as:

   for Test::Frame use (Payload => Test::Packet (Length));