Remove unused code

- Remove assignment of invalid field - Remove Successor function, was only used in said assignment For eng/RecordFlux/RecordFlux#1448
AdaCore · Nov 5, 2023 · ee47a40 · ee47a40
1 parent e1cf41e
commit ee47a40
Show file tree

Hide file tree

Showing 24 changed files with 1 addition and 751 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -15,6 +15,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 
 - Syntax for passing repeated `-i` and `-v` options to `rflx validate` (eng/recordflux/RecordFlux#1441)
+- Simplified setter code and removed internal `Successor` function (eng/recordflux/RecordFlux#1448)
 
 ### Fixed
 

diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -708,19 +708,6 @@ def initialize_field_statements(
                 ("Value", Number(0)),
             ),
         ),
-        Assignment(
-            Indexed(
-                Variable("Ctx.Cursors"),
-                Call(
-                    "Successor",
-                    [Variable("Ctx"), Variable(field.affixed_name)],
-                ),
-            ),
-            NamedAggregate(
-                ("State", Variable("S_Invalid")),
-                ("others", Variable("<>")),
-            ),
-        ),
     ]
 
 

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -577,12 +577,6 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:  # noqa: PLR0912
                 scalar_fields,
                 composite_fields,
             ),
-            self._executor.submit(
-                message_generator.create_successor_function,
-                self._prefix,
-                message,
-                sequence_fields,
-            ),
             self._executor.submit(
                 message_generator.create_invalid_successor_function,
                 message,

diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -2220,76 +2220,6 @@ def condition(field: Field, message: Message) -> Expr:
     )
 
 
-def create_successor_function(
-    prefix: str,
-    message: Message,
-    sequence_fields: abc.Mapping[Field, Type],
-) -> UnitPart:
-    if (
-        len(sequence_fields) == 0
-        and len([t for t in message.field_types.values() if isinstance(t, (Opaque, Sequence))]) == 0
-    ):
-        return UnitPart()
-    specification = FunctionSpecification(
-        "Successor",
-        "Virtual_Field",
-        [Parameter(["Ctx"], "Context"), Parameter(["Fld"], "Field")],
-    )
-
-    return UnitPart(
-        [],
-        common.wrap_warning(
-            [
-                ExpressionFunctionDeclaration(
-                    specification,
-                    Case(
-                        Variable("Fld"),
-                        [
-                            (
-                                Variable(f.affixed_name),
-                                If(
-                                    [
-                                        (
-                                            l.condition.substituted(
-                                                common.substitution(message, prefix),
-                                            )
-                                            .simplified()
-                                            .ada_expr(),
-                                            Variable(l.target.affixed_name),
-                                        )
-                                        for l in message.outgoing(f)
-                                    ],
-                                    Variable(INITIAL.affixed_name),
-                                ),
-                            )
-                            for f in message.fields
-                        ],
-                    ),
-                    [
-                        Precondition(
-                            And(
-                                Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
-                                Call(
-                                    prefix * message.identifier * "Well_Formed",
-                                    [Variable("Ctx"), Variable("Fld")],
-                                ),
-                                Call(
-                                    prefix * message.identifier * "Valid_Next",
-                                    [Variable("Ctx"), Variable("Fld")],
-                                ),
-                            ),
-                        ),
-                    ],
-                ),
-            ],
-            [
-                # Eng/RecordFlux/Workarounds#31
-                "precondition is always False",
-            ],
-        ),
-    )
-
-
 def create_invalid_successor_function(message: Message, requires_set_procedure: bool) -> UnitPart:
     if len(message.fields) == 1 or not requires_set_procedure:
         return UnitPart()

diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb
@@ -67,20 +67,6 @@ is
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
    end Data;
 
-   pragma Warnings (Off, "precondition is always False");
-
-   function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
-     ((case Fld is
-          when F_Data =>
-             F_Final))
-    with
-     Pre =>
-       RFLX.Test.Message.Has_Buffer (Ctx)
-       and RFLX.Test.Message.Well_Formed (Ctx, Fld)
-       and RFLX.Test.Message.Valid_Next (Ctx, Fld);
-
-   pragma Warnings (On, "precondition is always False");
-
    function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is
      (Ctx.Buffer /= null
       and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last
@@ -271,7 +257,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>);
    end Initialize_Data_Private;
 
    procedure Initialize_Data (Ctx : in out Context; Length : RFLX_Types.Length) is

diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.adb b/tests/feature/parameterized_messages/generated/rflx-test-message.adb
@@ -67,31 +67,6 @@ is
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
    end Data;
 
-   pragma Warnings (Off, "precondition is always False");
-
-   function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
-     ((case Fld is
-          when F_Data =>
-             (if
-                 RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True))
-              then
-                 F_Extension
-              elsif
-                 RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (False))
-              then
-                 F_Final
-              else
-                 F_Initial),
-          when F_Extension =>
-             F_Final))
-    with
-     Pre =>
-       RFLX.Test.Message.Has_Buffer (Ctx)
-       and RFLX.Test.Message.Well_Formed (Ctx, Fld)
-       and RFLX.Test.Message.Valid_Next (Ctx, Fld);
-
-   pragma Warnings (On, "precondition is always False");
-
    function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is
      (Ctx.Buffer /= null
       and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last
@@ -258,7 +233,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>);
    end Initialize_Data_Private;
 
    procedure Initialize_Data (Ctx : in out Context) is
@@ -297,7 +271,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Extension) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Extension)) := (State => S_Invalid, others => <>);
    end Initialize_Extension_Private;
 
    procedure Initialize_Extension (Ctx : in out Context) is

diff --git a/tests/feature/session_functions/generated/rflx-test-definite_message.adb b/tests/feature/session_functions/generated/rflx-test-definite_message.adb
@@ -68,24 +68,6 @@ is
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
    end Data;
 
-   pragma Warnings (Off, "precondition is always False");
-
-   function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
-     ((case Fld is
-          when F_Message_Type =>
-             F_Length,
-          when F_Length =>
-             F_Data,
-          when F_Data =>
-             F_Final))
-    with
-     Pre =>
-       RFLX.Test.Definite_Message.Has_Buffer (Ctx)
-       and RFLX.Test.Definite_Message.Well_Formed (Ctx, Fld)
-       and RFLX.Test.Definite_Message.Valid_Next (Ctx, Fld);
-
-   pragma Warnings (On, "precondition is always False");
-
    function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
      ((case Fld is
           when F_Message_Type =>
@@ -396,7 +378,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>);
    end Initialize_Data_Private;
 
    procedure Initialize_Data (Ctx : in out Context) is

diff --git a/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb b/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb
@@ -68,22 +68,6 @@ is
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
    end Data;
 
-   pragma Warnings (Off, "precondition is always False");
-
-   function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
-     ((case Fld is
-          when F_Length =>
-             (if Ctx.Cursors (F_Length).Value > 1 then F_Data else F_Initial),
-          when F_Data =>
-             F_Final))
-    with
-     Pre =>
-       RFLX.Test.Option_Data.Has_Buffer (Ctx)
-       and RFLX.Test.Option_Data.Well_Formed (Ctx, Fld)
-       and RFLX.Test.Option_Data.Valid_Next (Ctx, Fld);
-
-   pragma Warnings (On, "precondition is always False");
-
    function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
      ((case Fld is
           when F_Length =>
@@ -353,7 +337,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>);
    end Initialize_Data_Private;
 
    procedure Initialize_Data (Ctx : in out Context) is

diff --git a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb
@@ -68,33 +68,6 @@ is
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
    end Data;
 
-   pragma Warnings (Off, "precondition is always False");
-
-   function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
-     ((case Fld is
-          when F_Tag =>
-             (if
-                 RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Error))
-              then
-                 F_Final
-              elsif
-                 RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Data))
-              then
-                 F_Length
-              else
-                 F_Initial),
-          when F_Length =>
-             F_Value,
-          when F_Value =>
-             F_Final))
-    with
-     Pre =>
-       RFLX.TLV.Message.Has_Buffer (Ctx)
-       and RFLX.TLV.Message.Well_Formed (Ctx, Fld)
-       and RFLX.TLV.Message.Valid_Next (Ctx, Fld);
-
-   pragma Warnings (On, "precondition is always False");
-
    function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
      ((case Fld is
           when F_Tag =>
@@ -384,7 +357,6 @@ is
       Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       Ctx.Cursors (F_Value) := (State => S_Well_Formed, First => First, Last => Last, Value => 0);
-      Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, others => <>);
    end Initialize_Value_Private;
 
    procedure Initialize_Value (Ctx : in out Context) is