Remove requirements tool and references for feature coverage

Ref. eng/recordflux/RecordFlux#1783
AdaCore · Sep 13, 2024 · c26f0c9 · c26f0c9
1 parent c1a2f37
commit c26f0c9
Show file tree

Hide file tree

Showing 44 changed files with 501 additions and 1,344 deletions.
diff --git a/doc/language_reference/language_reference.rst b/doc/language_reference/language_reference.rst
diff --git a/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb
@@ -82,7 +82,7 @@ is
       pragma Warnings (On, "this code can never be executed and has been deleted");
       pragma Warnings (On, "condition is always False");
       pragma Warnings (On, "condition can only be False if invalid values present");
-      -- tests/feature/fsm_append_unconstrained/test.rflx:14:10
+      -- tests/feature/fsm_append_unconstrained/test.rflx:13:10
       if not Universal.Options.Has_Element (Options_Ctx) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Start_Invariant);
@@ -185,7 +185,7 @@ is
       pragma Warnings (On, "this code can never be executed and has been deleted");
       pragma Warnings (On, "condition is always False");
       pragma Warnings (On, "condition can only be False if invalid values present");
-      -- tests/feature/fsm_append_unconstrained/test.rflx:16:10
+      -- tests/feature/fsm_append_unconstrained/test.rflx:14:10
       if not Universal.Options.Has_Element (Options_Ctx) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Start_Invariant);
@@ -288,7 +288,7 @@ is
       pragma Warnings (On, "this code can never be executed and has been deleted");
       pragma Warnings (On, "condition is always False");
       pragma Warnings (On, "condition can only be False if invalid values present");
-      -- tests/feature/fsm_append_unconstrained/test.rflx:18:10
+      -- tests/feature/fsm_append_unconstrained/test.rflx:15:10
       if not Universal.Options.Has_Element (Options_Ctx) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Start_Invariant);
@@ -319,7 +319,7 @@ is
          Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx);
          pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call");
       end;
-      -- tests/feature/fsm_append_unconstrained/test.rflx:20:10
+      -- tests/feature/fsm_append_unconstrained/test.rflx:16:10
       Universal.Message.Reset (Ctx.P.Message_Ctx);
       if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then
          Ctx.P.Next_State := S_Final;
@@ -381,7 +381,7 @@ is
         Ghost;
    begin
       pragma Assert (Reply_Invariant);
-      -- tests/feature/fsm_append_unconstrained/test.rflx:29:10
+      -- tests/feature/fsm_append_unconstrained/test.rflx:25:10
       Ctx.P.Next_State := S_Final;
       pragma Assert (Reply_Invariant);
    end Reply;

diff --git a/tests/feature/fsm_append_unconstrained/test.rflx b/tests/feature/fsm_append_unconstrained/test.rflx
@@ -3,32 +3,28 @@ with Universal;
 package Test is
 
    generic
-      Channel : Channel with Writable; -- §S-P-C-W
+      Channel : Channel with Writable;
    machine S is
-      Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
+      Message : Universal::Message;
    begin
       state Start is
-         Options : Universal::Options; -- §S-S-D-V-T-MS, §S-S-D-V-E-N
+         Options : Universal::Options;
       begin
-         -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L
          Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 1, Data => [1]));
-         -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L
          Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [2, 3]));
-         -- §S-S-A-AP-MA
          Options'Append (Universal::Option'(Option_Type => Universal::OT_Null));
-         -- §S-S-A-A-MA
          Message := Universal::Message'(Message_Type => Universal::MT_Unconstrained_Options, Options => Options);
       transition
-         goto Reply -- §S-S-T-N
+         goto Reply
       exception
-         goto null -- §S-S-E
+         goto null
       end Start;
 
       state Reply is
       begin
-         Channel'Write (Message); -- §S-S-A-WR-V
+         Channel'Write (Message);
       transition
-         goto null -- §S-S-T-N
+         goto null
       end Reply;
    end S;
 

diff --git a/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb
@@ -81,7 +81,7 @@ is
       pragma Warnings (On, "condition can only be False if invalid values present");
       -- tests/feature/fsm_case_expression_aggregate/test.rflx:24:10
       Recv_Type := Universal.Message.Get_Message_Type (Ctx.P.Message_Ctx);
-      -- tests/feature/fsm_case_expression_aggregate/test.rflx:26:10
+      -- tests/feature/fsm_case_expression_aggregate/test.rflx:25:10
       Universal.Message.Reset (Ctx.P.Message_Ctx);
       if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then
          Ctx.P.Next_State := S_Final;
@@ -165,7 +165,7 @@ is
         Ghost;
    begin
       pragma Assert (Reply_Invariant);
-      -- tests/feature/fsm_case_expression_aggregate/test.rflx:45:10
+      -- tests/feature/fsm_case_expression_aggregate/test.rflx:44:10
       Ctx.P.Next_State := S_Final;
       pragma Assert (Reply_Invariant);
    end Reply;

diff --git a/tests/feature/fsm_case_expression_aggregate/test.rflx b/tests/feature/fsm_case_expression_aggregate/test.rflx
@@ -3,29 +3,28 @@ with Universal;
 package Test is
 
    generic
-      Channel : Channel with Readable, Writable; -- §S-P-C-RW
+      Channel : Channel with Readable, Writable;
    machine S is
-      Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
+      Message : Universal::Message;
    begin
       state Start is
       begin
-         Channel'Read (Message); -- §S-S-A-RD-V
+         Channel'Read (Message);
       transition
          goto Prepare
-            if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V
-         goto null -- §S-S-T-N
+            if Message'Valid
+         goto null
       exception
-         goto null -- §S-S-E
+         goto null
       end Start;
 
       state Prepare is
-         Recv_Type : Universal::Message_Type; -- §S-D-V-T-SC
+         Recv_Type : Universal::Message_Type;
       begin
-         Recv_Type := Message.Message_Type; -- §S-S-A-A-V
-         -- §S-S-A-A-MA
+         Recv_Type := Message.Message_Type;
          Message := Universal::Message'(Message_Type => Universal::MT_Value,
                                         Length       => 1,
-                                        Value        => -- §S-E-CE
+                                        Value        =>
                                                         (case Recv_Type is
                                                             when Universal::MT_Null | Universal::MT_Data =>   2,
                                                             when Universal::MT_Value                     =>   4,
@@ -35,16 +34,16 @@ package Test is
                                                             when Universal::MT_Unconstrained_Data        =>  64,
                                                             when Universal::MT_Unconstrained_Options     => 128));
       transition
-         goto Reply -- §S-S-T-N
+         goto Reply
       exception
-         goto null -- §S-S-E
+         goto null
       end Prepare;
 
       state Reply is
       begin
-         Channel'Write (Message); -- §S-S-A-WR-V
+         Channel'Write (Message);
       transition
-         goto null -- §S-S-T-N
+         goto null
       end Reply;
    end S;
 

diff --git a/tests/feature/fsm_case_expression_numeric/test.rflx b/tests/feature/fsm_case_expression_numeric/test.rflx
@@ -10,41 +10,41 @@ package Test is
       end message;
 
    generic
-      Channel : Channel with Readable, Writable; -- §S-P-C-RW
+      Channel : Channel with Readable, Writable;
    machine S is
-      Message : Message; -- §S-D-V-T-M, §S-D-V-E-N
+      Message : Message;
    begin
       state Start is
       begin
-         Channel'Read (Message); -- §S-S-A-RD-V
+         Channel'Read (Message);
       transition
          goto Prepare
-            if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V
-         goto null -- §S-S-T-N
+            if Message'Valid
+         goto null
       exception
-         goto null -- §S-S-E
+         goto null
       end Start;
 
       state Prepare is
          Value : Tiny_Int;
       begin
-         Value := (case Message.Value is  -- §S-E-CE
+         Value := (case Message.Value is
                       when 1 | 2 => 4,
                       when 3     => 1,
                       when 4     => 2);
-         -- §S-S-A-A-MA
+
          Message := Message'(Value => Value);
       transition
-         goto Reply -- §S-S-T-N
+         goto Reply
       exception
-         goto null -- §S-S-E
+         goto null
       end Prepare;
 
       state Reply is
       begin
-         Channel'Write (Message); -- §S-S-A-WR-V
+         Channel'Write (Message);
       transition
-         goto null -- §S-S-T-N
+         goto null
       end Reply;
    end S;
 

diff --git a/tests/feature/fsm_channel_multiplexing/test.rflx b/tests/feature/fsm_channel_multiplexing/test.rflx
@@ -3,39 +3,39 @@ with Universal;
 package Test is
 
    generic
-      I_1 : Channel with Readable; -- §S-P-C-R
-      I_2 : Channel with Readable; -- §S-P-C-R
-      O : Channel with Writable; -- §S-P-C-W
+      I_1 : Channel with Readable;
+      I_2 : Channel with Readable;
+      O : Channel with Writable;
    machine S is
-      Message_1 : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
-      Message_2 : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
+      Message_1 : Universal::Message;
+      Message_2 : Universal::Message;
    begin
       state Start is
       begin
-         I_1'Read (Message_1); -- §S-S-A-RD-V
-         I_2'Read (Message_2); -- §S-S-A-RD-V
+         I_1'Read (Message_1);
+         I_2'Read (Message_2);
       transition
          goto Reply_1
-            if Message_1'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V
+            if Message_1'Has_Data
          goto Reply_2
-            if Message_2'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V
-         goto null -- §S-S-E
+            if Message_2'Has_Data
+         goto null
       exception
-         goto null -- §S-S-E
+         goto null
       end Start;
 
       state Reply_1 is
       begin
-         O'Write (Message_1); -- §S-S-A-WR-V
+         O'Write (Message_1);
       transition
-         goto Start -- §S-S-T-N
+         goto Start
       end Reply_1;
 
       state Reply_2 is
       begin
-         O'Write (Message_2); -- §S-S-A-WR-V
+         O'Write (Message_2);
       transition
-         goto Start -- §S-S-T-N
+         goto Start
       end Reply_2;
    end S;
 

diff --git a/tests/feature/fsm_channels/test.rflx b/tests/feature/fsm_channels/test.rflx
@@ -3,27 +3,27 @@ with Universal;
 package Test is
 
    generic
-      I : Channel with Readable; -- §S-P-C-RW
-      O : Channel with Writable; -- §S-P-C-RW
+      I : Channel with Readable;
+      O : Channel with Writable;
    machine S is
-      Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N
+      Message : Universal::Message;
    begin
       state Start is
       begin
-         I'Read (Message); -- §S-S-A-RD-V
+         I'Read (Message);
       transition
          goto Reply
-            if Message'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V
-         goto null -- §S-S-T-N
+            if Message'Has_Data
+         goto null
       exception
-         goto null -- §S-S-E
+         goto null
       end Start;
 
       state Reply is
       begin
-         O'Write (Message); -- §S-S-A-WR-V
+         O'Write (Message);
       transition
-         goto Start -- §S-S-T-N
+         goto Start
       end Reply;
    end S;