Skip to content

Delta message aggregate with assignment from 'Opaque generates invalid code #1141

@jklmnn

Description

@jklmnn

When using a delta message aggregate to assign a message field from a 'Opaque expression:

Option.Data := Option_Data'Opaque;

I get the following error:

rflx-test-session.adb:127:94: error: invalid operand types for operator "<"
rflx-test-session.adb:127:94: error: left operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:35, instance at rflx-rflx_types.ads:14
rflx-test-session.adb:127:94: error: right operand has type "Length" defined at rflx-universal.ads:74

Full reproducing spec:

with Universal; 
                                                           
package Test is 

   type Result is (M_Valid, M_Invalid) with Size => 2;
                                                           
   type Option_Data is
      message
         Length : Universal::Length;                                                                                  
         Data : Opaque
            with Size => Length * 8;
      end message;

   generic
      Channel : Channel with Readable, Writable; -- §S-P-C-RW
      -- §S-P-F-R-S
      with function Get_Option_Data
         (Data : Opaque)
      return Option_Data;
   session Session with
      Initial => Start,
      Final => Terminated
   is
      Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
      Option : Universal::Option;
   begin
      state Start is
      begin
         Channel'Read (Message); -- §S-S-A-RD-V
      transition
         goto Process
            if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V
               and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L
               and Message.Length = 3 -- §S-S-T-S, §S-E-S-V, §S-S-T-L
         goto Terminated -- §S-S-T-N
      end Start;

      state Process is
         Option_Data : Option_Data;
      begin
         -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S
         Option_Data := Get_Option_Data (Message.Data);
         Option'Reset;
         Option.Option_Type := Universal::OT_Data;
         Option.Length := Option_Data.Length;
         Option.Data := Option_Data'Opaque;
      transition
         goto Reply -- §S-S-T-N
      exception
         goto Terminated -- §S-S-E
      end Process;

      state Reply is
      begin
         Channel'Write (Option); -- §S-S-A-WR-V
      transition
         goto Terminated -- §S-S-T-N
      end Reply;

      state Terminated is null state; -- §S-S-N
   end Session;

end Test;

Metadata

Metadata

Assignees

No one assigned

    Labels

    buggeneratorRelated to generator package (SPARK code generation)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions