Function in session is called incorrectly in generated code

[jklmnn]

When a function is passed to a session and used as in this example:

package Test is

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

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

   generic
      Transport : Channel with Readable, Writable;
      with function Valid_Func return Boolean;
   session Session with
      Initial => Receive,
      Final => Error
   is
      Packet : Packet;
   begin
      state Receive
      is
         Valid : Boolean;
      begin
         Valid := Valid_Func;
         Transport'Read (Packet);
      transition
         then Send
            if Packet'Valid and Valid
         then Error
      end Receive;

      state Send
      is
      begin
         Transport'Write (Packet'(Length => 42 * 8,
                                  Payload => Packet'Opaque));
      transition
         then Receive
      exception
         then Error
      end Send;

      state Error is null state;
   end Session;

end Test;

the generated code expects a procedure but calls this procedure as if it was a function:

generic
   with function Transport_Has_Data return Boolean;
   with procedure Transport_Read (Buffer : out RFLX_Types.Bytes; Length : out RFLX_Types.Length);
   with procedure Transport_Write (Buffer : RFLX_Types.Bytes);
   with procedure Valid_Func (Valid_Func : out Boolean);
package RFLX.Test.Session with

...

   procedure Receive (State : out Session_State) with
     Pre =>     
       Initialized,                                                         
     Post =>                                                                                                 
       Initialized                                                       
   is                                                                                                       
      Valid : Boolean;                                                     
   begin                                       
      Valid := Valid_Func;
      declare               
         procedure Test_Packet_Write is new Test.Packet.Write (Transport_Read);
      begin     
         Test_Packet_Write (Packet_Ctx);
      end;               
      Test.Packet.Verify_Message (Packet_Ctx);
      if
        Test.Packet.Structural_Valid_Message (Packet_Ctx)
        and then Valid
      then
         State := S_Send;
      else
         State := S_Error;
      end if;
   end Receive;

This leads to the following error:

rflx-test-session.adb:26:16: error: missing argument for parameter "Valid_Func" in call to "VALID_FUNC" declared at rflx-test-session.ads:19

[kanigsson]

I also noticed this recently. The issue seems to be that the parser doesn't recognize the expression "Valid_Func" as a call, but as a variable. So it generates "Obj := Valid_Func;" which would be correct if Valid_Func was a variable, instead of Valid_Func (Obj) which is needed if it's a function call.

[senier]

While this is obviously a parser issue, I wonder whether we want to support this kind of usage. It implies that the function is either completely static or uses some undefined global state. I could imagine that this could cause some trouble in the generated SPARK code, too. @treiher, what do you think?

[treiher]

The parser is unable to differentiate a variable from a function call with no parameters, as both cases are syntactically identical. The semantics can be just determined after parsing during semantic analysis (model generation).

I wonder whether we want to support this kind of usage. It implies that the function is either completely static or uses some undefined global state. I could imagine that this could cause some trouble in the generated SPARK code, too. @treiher, what do you think?

I think there are use cases for such functions, e.g., for supplying configuration values to the generated SPARK code.