Message field not checked when passed directly into function

[jklmnn]

When a message field is passed directly as a function parameter into a function that returns a boolean in the spec the function that is generated for the state will contain an unused label:

package Test is

   type Tag is (A => 1,
                B => 2,
                C => 3) with Size => 8;

   type M is
      message
         T : Tag;
      end message;

   type Outer is
      message
         Inner : M;
      end message;

   generic
      Transport : Channel with Readable, Writable;
      with function Check_Tag (T : Tag) return Boolean;
   session Session with
      Initial => Init,
      Final => End_Session
   is
      Msg : Outer;
   begin
      state Init
      is
      begin
         Transport'Read (Msg);
      transition
         goto Modify
      end Init;

      state Modify
      is
         Result : Boolean;
      begin
         Result := Check_Tag (Msg.Inner_T);
      transition
         goto End_Session
            if Result
         goto End_Session
      exception
         goto End_Session
      end Modify;

      state End_Session is null state;

   end Session;

end Test;

The state Modify requires an exception transition and therefore generates the label <Finalize_Modify>. However this label is unused:

   procedure Modify (Ctx : in out Context'Class) with
     Pre =>
       Initialized (Ctx),        
     Post =>                             
       Initialized (Ctx)                                                                                                                                                                                                                    
   is                                                                                                                 
      Result : Boolean;                                                                                               
      function Modify_Invariant return Boolean is
        (Ctx.P.Slots.Slot_Ptr_1 = null)
       with                        
        Annotate =>                                        
          (GNATprove, Inline_For_Proof),         
        Ghost;                                                                                                        
   begin                      
      pragma Assert (Modify_Invariant);
      --  test.rflx:38:10
      Check_Tag (Ctx, Test.Outer.Get_Inner_T (Ctx.P.Msg_Ctx), Result);
      if Result then     
         Ctx.P.Next_State := S_End_Session;
      else            
         Ctx.P.Next_State := S_End_Session;                                                                           
      end if;
      pragma Assert (Modify_Invariant);
      <<Finalize_Modify>>
   end Modify;

If the return type of the function is something different it will be checked and the failing check generates a goto to Finalize_Modify. A boolean however is not checked and therefor this transition is not generated. Also the access to the message field should be checked. If the spec is changed that the message field is assigned to a variable first, this works:

      state Modify
      is
         Result : Boolean;
         T : Tag;
      begin
         T := Msg.Inner_T;
         Result := Check_Tag (T);
      transition
         goto End_Session
            if Result
         goto End_Session
      exception
         goto End_Session
      end Modify;

   procedure Modify (Ctx : in out Context'Class) with                                                                 
     Pre =>                                                                                                           
       Initialized (Ctx),                                                                                                                                                                                                                   
     Post =>    
       Initialized (Ctx)                                   
   is                                                                                                                 
      Result : Boolean;                                                                                               
      T : Test.Tag;      
      function Modify_Invariant return Boolean is
        (Ctx.P.Slots.Slot_Ptr_1 = null)
       with
        Annotate =>              
          (GNATprove, Inline_For_Proof), 
        Ghost;                                                                                                                                                                                                                              
   begin                                                                                                              
      pragma Assert (Modify_Invariant);                                                                               
      --  test.rflx:39:10
      if Test.Outer.Valid (Ctx.P.Msg_Ctx, Test.Outer.F_Inner_T) then
         T := Test.Outer.Get_Inner_T (Ctx.P.Msg_Ctx);
      else                                                 
         Ctx.P.Next_State := S_End_Session;      
         pragma Assert (Modify_Invariant);                                                                            
         goto Finalize_Modify;
      end if;          
      --  test.rflx:40:10
      Check_Tag (Ctx, T, Result);
      if Result then     
         Ctx.P.Next_State := S_End_Session;
      else            
         Ctx.P.Next_State := S_End_Session;                                                                                                                                                                                                 
      end if;
      pragma Assert (Modify_Invariant);
      <<Finalize_Modify>>
   end Modify;

[treiher]

The issue is caused by the nested expression Check_Tag (Msg.Inner_T) (the field access Msg.Inner_T inside the function call Check_Tag). Nested expressions are not yet supported (cf. #1019).