Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
jklmnn opened this issue Aug 18, 2022 · 0 comments
Open
Labels
bug generator Related to generator package (SPARK code generation)

Comments

@jklmnn
Copy link
Member

jklmnn commented Aug 18, 2022

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;
@jklmnn jklmnn added bug generator Related to generator package (SPARK code generation) labels Aug 18, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug generator Related to generator package (SPARK code generation)
Projects
None yet
Development

No branches or pull requests

1 participant