From fc96bb2a56fdb6f51de0320addc3894b7017e11a Mon Sep 17 00:00:00 2001
From: Johannes Kanig <kanig@adacore.com>
Date: Mon, 15 Jul 2024 09:21:34 +0900
Subject: [PATCH] Separate function for each field for Field_First

Ref. eng/recordflux/RecordFlux#1706
---
 CHANGELOG.md                                  |   2 +-
 rflx/generator/message.py                     | 104 ++++++-----
 .../boolean_variable/rflx-p-message.ads       |  25 ++-
 .../external_io_buffers/rflx-tlv-message.ads  |  35 +++-
 .../generated/rflx-test-m.ads                 |  45 +++--
 .../generated/rflx-test-message.ads           |  15 +-
 .../generated/rflx-test-message.ads           |  25 ++-
 .../generated/rflx-test-message.ads           |  15 +-
 .../generated/rflx-messages-msg.ads           |  25 ++-
 .../generated/rflx-messages-msg_le.ads        |  25 ++-
 .../generated/rflx-messages-msg_le_nested.ads |  35 +++-
 .../generated/rflx-test-definite_message.ads  |  35 +++-
 .../generated/rflx-test-option_data.ads       |  25 ++-
 .../generated/rflx-tlv-message.ads            |  35 +++-
 .../generated/rflx-universal-message.ads      | 121 ++++++++----
 .../generated/rflx-universal-option.ads       |  35 +++-
 .../generated/rflx-derivation-message.ads     |  35 +++-
 .../generated/rflx-enumeration-message.ads    |  15 +-
 tests/spark/generated/rflx-ethernet-frame.ads |  99 +++++++---
 .../generated/rflx-expression-message.ads     |  15 +-
 .../rflx-fixed_size-simple_message.ads        |  25 ++-
 tests/spark/generated/rflx-icmp-message.ads   | 171 +++++++++++++++--
 tests/spark/generated/rflx-ipv4-option.ads    |  55 +++++-
 tests/spark/generated/rflx-ipv4-packet.ads    | 175 +++++++++++++++---
 .../generated/rflx-sequence-inner_message.ads |  25 ++-
 .../spark/generated/rflx-sequence-message.ads |  45 ++++-
 .../rflx-sequence-messages_message.ads        |  25 ++-
 ...-sequence_size_defined_by_message_size.ads |  25 ++-
 tests/spark/generated/rflx-tlv-message.ads    |  35 +++-
 tests/spark/generated/rflx-udp-datagram.ads   |  55 +++++-
 30 files changed, 1101 insertions(+), 301 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0ffcf3f3a..4cd6828f8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,7 +21,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - LLVM exception in addition to Apache-2.0 for generated code (eng/recordflux/RecordFlux#1671)
 - Improve suggestions when a package name is not correct (eng/recordflux/RecordFlux#1611)
 - Severities of error messages (eng/recordflux/RecordFlux#1698, eng/recordflux/RecordFlux#1685)
-- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707)
+- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707, eng/recordflux/RecordFlux#1706)
 - Cache directory from `$HOME/.cache/RecordFlux` to `$PWD/.rflx_cache` (eng/recordflux/RecordFlux#1723)
 
 ### Fixed
diff --git a/rflx/generator/message.py b/rflx/generator/message.py
index a8d66252b..955f48a99 100644
--- a/rflx/generator/message.py
+++ b/rflx/generator/message.py
@@ -22,7 +22,6 @@
     Component,
     Constrained,
     ContractCases,
-    Decreases,
     DefaultInitialCondition,
     Depends,
     Discriminant,
@@ -79,7 +78,6 @@
     Sub,
     SubprogramBody,
     SubprogramDeclaration,
-    SubprogramVariant,
     UnitPart,
     UseTypeClause,
     ValueRange,
@@ -636,7 +634,7 @@ def create_field_size_internal_function(message: Message, prefix: str) -> UnitPa
 def create_field_first_internal_function(message: Message, prefix: str) -> UnitPart:
     def recursive_call(fld: Field) -> expr.Expr:
         return expr.Call(
-            "Field_First_Internal",
+            "Field_First_" + fld.name,
             rty.BIT_INDEX,
             [
                 expr.Variable("Cursors"),
@@ -645,7 +643,6 @@ def recursive_call(fld: Field) -> expr.Expr:
                 expr.Variable("Written_Last"),
                 expr.Variable("Buffer"),
                 *[expr.Variable(param.name) for param in message.parameter_types],
-                expr.Variable(fld.affixed_name),
             ],
         )
 
@@ -715,6 +712,63 @@ def fld_first_expr(fld: Field) -> expr.Expr:
             dist.substituted(field_size_substitution),
         ).simplified()
 
+    param_args = [Variable(param.name) for param in message.parameter_types]
+
+    def precond(fld: str) -> Precondition:
+        return Precondition(
+            AndThen(
+                Call(
+                    "Cursors_Invariant",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                    ],
+                ),
+                Call(
+                    "Valid_Predecessors_Invariant",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *param_args,
+                    ],
+                ),
+                Call(
+                    "Valid_Next_Internal",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *param_args,
+                        Variable(fld),
+                    ],
+                ),
+            ),
+        )
+
+    def fld_first_func(fld: Field) -> ExpressionFunctionDeclaration:
+        return ExpressionFunctionDeclaration(
+            FunctionSpecification(
+                "Field_First_" + fld.name,
+                "RFLX_Types.Bit_Index'Base",
+                [
+                    Parameter(["Cursors"], "Field_Cursors"),
+                    Parameter(["First"], const.TYPES_BIT_INDEX),
+                    Parameter(["Verified_Last"], const.TYPES_BIT_LENGTH),
+                    Parameter(["Written_Last"], const.TYPES_BIT_LENGTH),
+                    Parameter(["Buffer"], const.TYPES_BYTES_PTR),
+                    *common.message_parameters(message),
+                ],
+            ),
+            expr_conv.to_ada(fld_first_expr(fld)),
+            [precond(fld.affixed_name)],
+        )
+
     specification = FunctionSpecification(
         "Field_First_Internal",
         "RFLX_Types.Bit_Index'Base",
@@ -729,59 +783,23 @@ def fld_first_expr(fld: Field) -> expr.Expr:
         ],
     )
 
-    param_args = [Variable(param.name) for param in message.parameter_types]
-
     return UnitPart(
         [],
         private=common.wrap_warning(
             [
+                *[fld_first_func(fld) for fld in message.fields],
                 ExpressionFunctionDeclaration(
                     specification,
                     Case(
                         Variable("Fld"),
                         [
-                            (Variable(f.affixed_name), expr_conv.to_ada(fld_first_expr(f)))
+                            (Variable(f.affixed_name), expr_conv.to_ada(recursive_call(f)))
                             for f in message.fields
                         ],
                     ),
                     [
-                        Precondition(
-                            AndThen(
-                                Call(
-                                    "Cursors_Invariant",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                    ],
-                                ),
-                                Call(
-                                    "Valid_Predecessors_Invariant",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                        Variable("Written_Last"),
-                                        Variable("Buffer"),
-                                        *param_args,
-                                    ],
-                                ),
-                                Call(
-                                    "Valid_Next_Internal",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                        Variable("Written_Last"),
-                                        Variable("Buffer"),
-                                        *param_args,
-                                        Variable("Fld"),
-                                    ],
-                                ),
-                            ),
-                        ),
+                        precond("Fld"),
                         Postcondition(TRUE),
-                        SubprogramVariant(Decreases(Variable("Fld"))),
                     ],
                 ),
             ],
diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads
index 30230540d..30892d7aa 100644
--- a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads
+++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads
@@ -590,22 +590,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A);
+
+   function Field_First_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 1)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_A =>
-             First,
+             Field_First_A (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_B =>
-             First + 1))
+             Field_First_B (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads b/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads
index 58189cb51..97c86073f 100644
--- a/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads
+++ b/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads
@@ -702,24 +702,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Value =>
-             First + 24))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads
index 9e7ee98dc..d0888f1e0 100644
--- a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads
+++ b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads
@@ -560,32 +560,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_F1 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F1);
+
+   function Field_First_F2 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is
+     ((if
+          Well_Formed (Cursors (F_F1))
+          and then True
+       then
+          First + 8
+       elsif
+          True
+       then
+          First + 0
+       else
+          RFLX_Types.Unreachable))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F2);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_F1 =>
-             First,
+             Field_First_F1 (Cursors, First, Verified_Last, Written_Last, Buffer, P),
           when F_F2 =>
-             (if
-                 Well_Formed (Cursors (F_F1))
-                 and then True
-              then
-                 First + 8
-              elsif
-                 True
-              then
-                 First + 0
-              else
-                 RFLX_Types.Unreachable)))
+             Field_First_F2 (Cursors, First, Verified_Last, Written_Last, Buffer, P)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
index 1422502b6..2dbd428b6 100644
--- a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
+++ b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
@@ -611,20 +611,25 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Data =>
-             First))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads
index 290b4fe6b..eae3e29d3 100644
--- a/tests/feature/parameterized_messages/generated/rflx-test-message.ads
+++ b/tests/feature/parameterized_messages/generated/rflx-test-message.ads
@@ -710,22 +710,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data);
+
+   function Field_First_Extension (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Data =>
-             First,
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended),
           when F_Extension =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data)))
+             Field_First_Extension (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads b/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads
index 80bfc50a9..757999fff 100644
--- a/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads
+++ b/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads
@@ -548,20 +548,25 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Value =>
-             First))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg.ads b/tests/feature/session_endianness/generated/rflx-messages-msg.ads
index ccf29f6d5..0b2cad585 100644
--- a/tests/feature/session_endianness/generated/rflx-messages-msg.ads
+++ b/tests/feature/session_endianness/generated/rflx-messages-msg.ads
@@ -586,22 +586,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A);
+
+   function Field_First_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_A =>
-             First,
+             Field_First_A (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_B =>
-             First + 32))
+             Field_First_B (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads b/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads
index 7b31ee5d2..d69ef10f9 100644
--- a/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads
+++ b/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads
@@ -586,22 +586,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_C (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C);
+
+   function Field_First_D (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_C =>
-             First,
+             Field_First_C (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_D =>
-             First + 32))
+             Field_First_D (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads
index abda2059e..a2625039b 100644
--- a/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads
+++ b/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads
@@ -626,24 +626,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_X_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A);
+
+   function Field_First_X_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B);
+
+   function Field_First_Y (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 64)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_X_A =>
-             First,
+             Field_First_X_A (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_X_B =>
-             First + 32,
+             Field_First_X_B (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Y =>
-             First + 64))
+             Field_First_Y (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_functions/generated/rflx-test-definite_message.ads b/tests/feature/session_functions/generated/rflx-test-definite_message.ads
index 209903ebd..ff05e960f 100644
--- a/tests/feature/session_functions/generated/rflx-test-definite_message.ads
+++ b/tests/feature/session_functions/generated/rflx-test-definite_message.ads
@@ -735,24 +735,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Message_Type =>
-             First,
+             Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Data =>
-             First + 16))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads b/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads
index cfc8cb9aa..902ef6213 100644
--- a/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads
+++ b/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads
@@ -677,22 +677,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Length =>
-             First,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Data =>
-             First + 16))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads
index 58189cb51..97c86073f 100644
--- a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads
+++ b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads
@@ -702,24 +702,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Value =>
-             First + 24))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/shared/generated/rflx-universal-message.ads b/tests/feature/shared/generated/rflx-universal-message.ads
index 3a3141e29..f46d930d1 100644
--- a/tests/feature/shared/generated/rflx-universal-message.ads
+++ b/tests/feature/shared/generated/rflx-universal-message.ads
@@ -1305,52 +1305,107 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     ((if
+          Well_Formed (Cursors (F_Length))
+          and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Data))
+       then
+          First + 24
+       elsif
+          Well_Formed (Cursors (F_Message_Type))
+          and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data))
+       then
+          First + 8
+       else
+          RFLX_Types.Unreachable))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
+   function Field_First_Option_Types (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Types);
+
+   function Field_First_Options (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     ((if
+          Well_Formed (Cursors (F_Length))
+          and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Options))
+       then
+          First + 24
+       elsif
+          Well_Formed (Cursors (F_Message_Type))
+          and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options))
+       then
+          First + 8
+       else
+          RFLX_Types.Unreachable))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
+   function Field_First_Values (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Values);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Message_Type =>
-             First,
+             Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Data =>
-             (if
-                 Well_Formed (Cursors (F_Length))
-                 and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Data))
-              then
-                 First + 24
-              elsif
-                 Well_Formed (Cursors (F_Message_Type))
-                 and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data))
-              then
-                 First + 8
-              else
-                 RFLX_Types.Unreachable),
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Option_Types =>
-             First + 24,
+             Field_First_Option_Types (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Options =>
-             (if
-                 Well_Formed (Cursors (F_Length))
-                 and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Options))
-              then
-                 First + 24
-              elsif
-                 Well_Formed (Cursors (F_Message_Type))
-                 and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options))
-              then
-                 First + 8
-              else
-                 RFLX_Types.Unreachable),
-          when F_Value | F_Values =>
-             First + 24))
+             Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Value =>
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Values =>
+             Field_First_Values (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/feature/shared/generated/rflx-universal-option.ads b/tests/feature/shared/generated/rflx-universal-option.ads
index 4f18e2962..0201955d4 100644
--- a/tests/feature/shared/generated/rflx-universal-option.ads
+++ b/tests/feature/shared/generated/rflx-universal-option.ads
@@ -702,24 +702,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Option_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Type);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Option_Type =>
-             First,
+             Field_First_Option_Type (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Data =>
-             First + 24))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads
index eb8436da9..7ab82340e 100644
--- a/tests/spark/generated/rflx-derivation-message.ads
+++ b/tests/spark/generated/rflx-derivation-message.ads
@@ -704,24 +704,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Value =>
-             First + 24))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads
index bf0babdcd..389effc2d 100644
--- a/tests/spark/generated/rflx-enumeration-message.ads
+++ b/tests/spark/generated/rflx-enumeration-message.ads
@@ -548,20 +548,25 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Priority (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Priority);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Priority =>
-             First))
+             Field_First_Priority (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads
index 45789a6c3..bc534a9fd 100644
--- a/tests/spark/generated/rflx-ethernet-frame.ads
+++ b/tests/spark/generated/rflx-ethernet-frame.ads
@@ -865,41 +865,96 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Destination (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination);
+
+   function Field_First_Source (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 48)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source);
+
+   function Field_First_Type_Length_TPID (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 96)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length_TPID);
+
+   function Field_First_TPID (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 96)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TPID);
+
+   function Field_First_TCI (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 112)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TCI);
+
+   function Field_First_Type_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     ((if
+          Well_Formed (Cursors (F_TCI))
+          and then True
+       then
+          First + 128
+       elsif
+          Well_Formed (Cursors (F_Type_Length_TPID))
+          and then Cursors (F_Type_Length_TPID).Value /= 16#8100#
+       then
+          First + 96
+       else
+          RFLX_Types.Unreachable))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length);
+
+   function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Type_Length (Cursors, First, Verified_Last, Written_Last, Buffer) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Destination =>
-             First,
+             Field_First_Destination (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Source =>
-             First + 48,
-          when F_Type_Length_TPID | F_TPID =>
-             First + 96,
+             Field_First_Source (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Type_Length_TPID =>
+             Field_First_Type_Length_TPID (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_TPID =>
+             Field_First_TPID (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_TCI =>
-             First + 112,
+             Field_First_TCI (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Type_Length =>
-             (if
-                 Well_Formed (Cursors (F_TCI))
-                 and then True
-              then
-                 First + 128
-              elsif
-                 Well_Formed (Cursors (F_Type_Length_TPID))
-                 and then Cursors (F_Type_Length_TPID).Value /= 16#8100#
-              then
-                 First + 96
-              else
-                 RFLX_Types.Unreachable),
+             Field_First_Type_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Payload =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length) + 16))
+             Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads
index 6117d0d9a..c2c21d50e 100644
--- a/tests/spark/generated/rflx-expression-message.ads
+++ b/tests/spark/generated/rflx-expression-message.ads
@@ -620,20 +620,25 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Payload =>
-             First))
+             Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads
index 898cafb60..d0aa78c33 100644
--- a/tests/spark/generated/rflx-fixed_size-simple_message.ads
+++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads
@@ -680,22 +680,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Message_Type =>
-             First,
+             Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Data =>
-             First + 8))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads
index 09e585b1b..a6eafeaa4 100644
--- a/tests/spark/generated/rflx-icmp-message.ads
+++ b/tests/spark/generated/rflx-icmp-message.ads
@@ -1434,36 +1434,175 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Code_Destination_Unreachable (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Destination_Unreachable);
+
+   function Field_First_Code_Redirect (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Redirect);
+
+   function Field_First_Code_Time_Exceeded (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Time_Exceeded);
+
+   function Field_First_Code_Zero (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Zero);
+
+   function Field_First_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum);
+
+   function Field_First_Gateway_Internet_Address (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Gateway_Internet_Address);
+
+   function Field_First_Identifier (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Identifier);
+
+   function Field_First_Pointer (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Pointer);
+
+   function Field_First_Unused_32 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Unused_32);
+
+   function Field_First_Sequence_Number (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Sequence_Number);
+
+   function Field_First_Unused_24 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Unused_24);
+
+   function Field_First_Originate_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 48)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Originate_Timestamp);
+
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 48)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
+   function Field_First_Receive_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 80)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Receive_Timestamp);
+
+   function Field_First_Transmit_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 112)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Transmit_Timestamp);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
-          when F_Code_Destination_Unreachable | F_Code_Redirect | F_Code_Time_Exceeded | F_Code_Zero =>
-             First + 8,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Code_Destination_Unreachable =>
+             Field_First_Code_Destination_Unreachable (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Code_Redirect =>
+             Field_First_Code_Redirect (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Code_Time_Exceeded =>
+             Field_First_Code_Time_Exceeded (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Code_Zero =>
+             Field_First_Code_Zero (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Checksum =>
-             First + 16,
-          when F_Gateway_Internet_Address | F_Identifier | F_Pointer | F_Unused_32 =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 16,
+             Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Gateway_Internet_Address =>
+             Field_First_Gateway_Internet_Address (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Identifier =>
+             Field_First_Identifier (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Pointer =>
+             Field_First_Pointer (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Unused_32 =>
+             Field_First_Unused_32 (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Sequence_Number =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 32,
+             Field_First_Sequence_Number (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Unused_24 =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 24,
-          when F_Originate_Timestamp | F_Data =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 48,
+             Field_First_Unused_24 (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Originate_Timestamp =>
+             Field_First_Originate_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer),
+          when F_Data =>
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Receive_Timestamp =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 80,
+             Field_First_Receive_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Transmit_Timestamp =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 112))
+             Field_First_Transmit_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads
index f5167248e..8d2be6a49 100644
--- a/tests/spark/generated/rflx-ipv4-option.ads
+++ b/tests/spark/generated/rflx-ipv4-option.ads
@@ -827,28 +827,65 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Copied (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Copied);
+
+   function Field_First_Option_Class (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 1)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Class);
+
+   function Field_First_Option_Number (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 3)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Number);
+
+   function Field_First_Option_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Length);
+
+   function Field_First_Option_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Copied =>
-             First,
+             Field_First_Copied (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Option_Class =>
-             First + 1,
+             Field_First_Option_Class (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Option_Number =>
-             First + 3,
+             Field_First_Option_Number (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Option_Length =>
-             First + 8,
+             Field_First_Option_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Option_Data =>
-             First + 16))
+             Field_First_Option_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads
index b132054cd..ffcd4445a 100644
--- a/tests/spark/generated/rflx-ipv4-packet.ads
+++ b/tests/spark/generated/rflx-ipv4-packet.ads
@@ -1590,52 +1590,185 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Version (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Version);
+
+   function Field_First_IHL (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 4)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_IHL);
+
+   function Field_First_DSCP (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_DSCP);
+
+   function Field_First_ECN (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 14)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_ECN);
+
+   function Field_First_Total_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Total_Length);
+
+   function Field_First_Identification (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Identification);
+
+   function Field_First_Flag_R (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 48)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_R);
+
+   function Field_First_Flag_DF (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 49)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_DF);
+
+   function Field_First_Flag_MF (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 50)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_MF);
+
+   function Field_First_Fragment_Offset (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 51)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Fragment_Offset);
+
+   function Field_First_TTL (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 64)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TTL);
+
+   function Field_First_Protocol (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 72)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Protocol);
+
+   function Field_First_Header_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 80)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Header_Checksum);
+
+   function Field_First_Source (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 96)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source);
+
+   function Field_First_Destination (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 128)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination);
+
+   function Field_First_Options (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 160)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options);
+
+   function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Version =>
-             First,
+             Field_First_Version (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_IHL =>
-             First + 4,
+             Field_First_IHL (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_DSCP =>
-             First + 8,
+             Field_First_DSCP (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_ECN =>
-             First + 14,
+             Field_First_ECN (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Total_Length =>
-             First + 16,
+             Field_First_Total_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Identification =>
-             First + 32,
+             Field_First_Identification (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Flag_R =>
-             First + 48,
+             Field_First_Flag_R (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Flag_DF =>
-             First + 49,
+             Field_First_Flag_DF (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Flag_MF =>
-             First + 50,
+             Field_First_Flag_MF (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Fragment_Offset =>
-             First + 51,
+             Field_First_Fragment_Offset (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_TTL =>
-             First + 64,
+             Field_First_TTL (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Protocol =>
-             First + 72,
+             Field_First_Protocol (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Header_Checksum =>
-             First + 80,
+             Field_First_Header_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Source =>
-             First + 96,
+             Field_First_Source (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Destination =>
-             First + 128,
+             Field_First_Destination (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Options =>
-             First + 160,
+             Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Payload =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options)))
+             Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads
index ece5dff53..ef5bc56ff 100644
--- a/tests/spark/generated/rflx-sequence-inner_message.ads
+++ b/tests/spark/generated/rflx-sequence-inner_message.ads
@@ -690,22 +690,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Length =>
-             First,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Payload =>
-             First + 8))
+             Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads
index 2e7a2738e..ee2833028 100644
--- a/tests/spark/generated/rflx-sequence-message.ads
+++ b/tests/spark/generated/rflx-sequence-message.ads
@@ -931,26 +931,55 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Integer_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector);
+
+   function Field_First_Enumeration_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Enumeration_Vector);
+
+   function Field_First_AV_Enumeration_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_AV_Enumeration_Vector);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Length =>
-             First,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Integer_Vector =>
-             First + 8,
+             Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Enumeration_Vector =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector),
+             Field_First_Enumeration_Vector (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_AV_Enumeration_Vector =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + 16))
+             Field_First_AV_Enumeration_Vector (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads
index 6372c2217..60ca18002 100644
--- a/tests/spark/generated/rflx-sequence-messages_message.ads
+++ b/tests/spark/generated/rflx-sequence-messages_message.ads
@@ -675,22 +675,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Messages (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Messages);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Length =>
-             First,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Messages =>
-             First + 8))
+             Field_First_Messages (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads
index ce49bff7d..8af34c507 100644
--- a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads
+++ b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads
@@ -677,22 +677,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Header (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Header);
+
+   function Field_First_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Vector);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Header =>
-             First,
+             Field_First_Header (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Vector =>
-             First + 8))
+             Field_First_Vector (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads
index 58189cb51..97c86073f 100644
--- a/tests/spark/generated/rflx-tlv-message.ads
+++ b/tests/spark/generated/rflx-tlv-message.ads
@@ -702,24 +702,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Value =>
-             First + 24))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 
diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads
index 5204da7ce..b190a22d4 100644
--- a/tests/spark/generated/rflx-udp-datagram.ads
+++ b/tests/spark/generated/rflx-udp-datagram.ads
@@ -825,28 +825,65 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Source_Port (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source_Port);
+
+   function Field_First_Destination_Port (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 16)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination_Port);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 32)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 48)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum);
+
+   function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 64)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Source_Port =>
-             First,
+             Field_First_Source_Port (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Destination_Port =>
-             First + 16,
+             Field_First_Destination_Port (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 32,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Checksum =>
-             First + 48,
+             Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Payload =>
-             First + 64))
+             Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");