Fix missing type information in Reset statement

Ref. #1080

CHANGELOG.md

@@ -79,6 +79,7 @@ Model:
 - Handling of `Message` attributes in message types (#729)
 - Missing file location in error messages (#647)
 - Bug box due to dangling field when merging messages (#1033)
+- Missing type information in `Reset` statement (#1080)
 
 Generator:
 

rflx/model/statement.py

@@ -196,6 +196,9 @@ def check_type(
         self, statement_type: rty.Type, typify_variable: Callable[[Expr], Expr]
     ) -> RecordFluxError:
         self.type_ = statement_type
+        self.associations = {
+            i: e.substituted(typify_variable) for i, e in self.associations.items()
+        }
         return rty.check_type_instance(
             statement_type,
             (rty.Sequence, rty.Message),

tests/integration/parameterized_messages/config.yml

@@ -10,6 +10,7 @@ sequence: |
   State: Process
   Read C: 1 2 3 4
   State: Reply
+  State: Reset
 prove:
   - rflx-test
   - rflx-test-message

tests/integration/parameterized_messages/generated/rflx-test-session.adb

@@ -73,6 +73,8 @@ is
    begin
       pragma Assert (Process_Invariant);
       --  tests/integration/parameterized_messages/test.rflx:49:10
+      Test.Message.Reset (Ctx.P.M_S_Ctx, Length => Ctx.P.M_R_Ctx.Length, Extended => True);
+      --  tests/integration/parameterized_messages/test.rflx:50:10
       if
          Test.Message.Size (Ctx.P.M_R_Ctx) <= 32768
          and then Test.Message.Size (Ctx.P.M_R_Ctx) mod RFLX_Types.Byte'Size = 0
@@ -158,7 +160,7 @@ is
          pragma Assert (Process_Invariant);
          goto Finalize_Process;
       end if;
-      --  tests/integration/parameterized_messages/test.rflx:50:10
+      --  tests/integration/parameterized_messages/test.rflx:51:10
       Length := Ctx.P.M_S_Ctx.Length;
       if Length = Ctx.P.M_R_Ctx.Length then
          Ctx.P.Next_State := S_Reply;
@@ -184,11 +186,32 @@ is
         Ghost;
    begin
       pragma Assert (Reply_Invariant);
-      --  tests/integration/parameterized_messages/test.rflx:62:10
-      Ctx.P.Next_State := S_Terminated;
+      --  tests/integration/parameterized_messages/test.rflx:63:10
+      Ctx.P.Next_State := S_Reset;
       pragma Assert (Reply_Invariant);
    end Reply;
 
+   procedure Reset (Ctx : in out Context'Class) with
+     Pre =>
+       Initialized (Ctx),
+     Post =>
+       Initialized (Ctx)
+   is
+      function Reset_Invariant return Boolean is
+        (Ctx.P.Slots.Slot_Ptr_1 = null
+         and Ctx.P.Slots.Slot_Ptr_2 = null)
+       with
+        Annotate =>
+          (GNATprove, Inline_For_Proof),
+        Ghost;
+   begin
+      pragma Assert (Reset_Invariant);
+      --  tests/integration/parameterized_messages/test.rflx:71:10
+      Test.Message.Reset (Ctx.P.M_S_Ctx, Length => Ctx.P.M_R_Ctx.Length, Extended => Ctx.P.M_R_Ctx.Extended);
+      Ctx.P.Next_State := S_Terminated;
+      pragma Assert (Reset_Invariant);
+   end Reset;
+
    procedure Error (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),
@@ -255,7 +278,7 @@ is
             null;
          when S_Receive =>
             Test.Message.Reset (Ctx.P.M_R_Ctx, Ctx.P.M_R_Ctx.First, Ctx.P.M_R_Ctx.First - 1, Ctx.P.M_R_Ctx.Length, Ctx.P.M_R_Ctx.Extended);
-         when S_Process | S_Reply | S_Error | S_Terminated =>
+         when S_Process | S_Reply | S_Reset | S_Error | S_Terminated =>
             null;
       end case;
    end Reset_Messages_Before_Write;
@@ -271,6 +294,8 @@ is
             Process (Ctx);
          when S_Reply =>
             Reply (Ctx);
+         when S_Reset =>
+            Reset (Ctx);
          when S_Error =>
             Error (Ctx);
          when S_Terminated =>

tests/integration/parameterized_messages/generated/rflx-test-session.ads

@@ -15,7 +15,7 @@ is
 
    type Channel is (C_C);
 
-   type State is (S_Start, S_Receive, S_Process, S_Reply, S_Error, S_Terminated);
+   type State is (S_Start, S_Receive, S_Process, S_Reply, S_Reset, S_Error, S_Terminated);
 
    type Private_Context is private;
 

tests/integration/parameterized_messages/test.rflx

@@ -46,6 +46,7 @@ package Test is
       is
          Length : Length;
       begin
+         M_S'Reset (Length => M_R.Length, Extended => True);
          M_S := Message'(Length => M_R.Length, Extended => True, Data => M_R.Data, Extension => [3, 4]);
          Length := M_S.Length;
       transition
@@ -61,9 +62,17 @@ package Test is
       begin
          C'Write (M_S);
       transition
-         goto Terminated
+         goto Reset
       end Reply;
 
+      state Reset
+      is
+      begin
+         M_S'Reset (Length => M_R.Length, Extended => M_R.Extended);
+      transition
+         goto Terminated
+      end Reset;
+
       state Error
       is
       begin