generated code

AdaCore · Aug 31, 2023 · e391995 · e391995
1 parent 4701fae
commit e391995
Show file tree

Hide file tree

Showing 25 changed files with 450 additions and 200 deletions.
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
@@ -548,6 +548,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -569,14 +586,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then (True)
       and then (True)
       and then ((if

diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads
@@ -660,6 +660,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -681,14 +698,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_Extension))
                  then

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
@@ -482,6 +482,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -503,14 +520,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then (True)
       and then (True)
       and then ((if

diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg.ads b/tests/feature/session_endianness/generated/rflx-messages-msg.ads
@@ -518,6 +518,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -539,14 +556,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if Well_Formed (Cursors (F_B)) then (Valid (Cursors (F_A)) and then Cursors (F_B).Predecessor = F_A)))
       and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B))))
       and then ((if

diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads b/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads
@@ -518,6 +518,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -539,14 +556,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if Well_Formed (Cursors (F_D)) then (Valid (Cursors (F_C)) and then Cursors (F_D).Predecessor = F_C)))
       and then ((if Invalid (Cursors (F_C)) then Invalid (Cursors (F_D))))
       and then ((if

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
@@ -556,6 +556,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -577,14 +594,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_X_B))
                  then

diff --git a/tests/feature/session_functions/generated/rflx-test-definite_message.ads b/tests/feature/session_functions/generated/rflx-test-definite_message.ads
@@ -666,6 +666,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -687,14 +704,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

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
@@ -604,6 +604,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -625,14 +642,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then

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
@@ -627,6 +627,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -648,14 +665,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

diff --git a/tests/feature/shared/generated/rflx-universal-message.ads b/tests/feature/shared/generated/rflx-universal-message.ads
@@ -1166,6 +1166,23 @@ private
      (Cursor.State = S_Invalid
       or Cursor.State = S_Incomplete);
 
+   pragma Warnings (Off, "postcondition does not mention function result");
+
+   function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is
+     ((for all F in Field =>
+          (if
+              Well_Formed (Cursors (F))
+           then
+              Cursors (F).First >= First
+              and Cursors (F).Last <= Verified_Last
+              and Cursors (F).First <= Cursors (F).Last + 1
+              and Valid_Value (F, Cursors (F).Value))))
+    with
+     Post =>
+       True;
+
+   pragma Warnings (On, "postcondition does not mention function result");
+
    pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type");
 
    pragma Warnings (Off, "postcondition does not mention function result");
@@ -1187,14 +1204,7 @@ private
       and then Last rem RFLX_Types.Byte'Size = 0
       and then Verified_Last rem RFLX_Types.Byte'Size = 0
       and then Written_Last rem RFLX_Types.Byte'Size = 0
-      and then (for all F in Field =>
-                   (if
-                       Well_Formed (Cursors (F))
-                    then
-                       Cursors (F).First >= First
-                       and Cursors (F).Last <= Verified_Last
-                       and Cursors (F).First <= Cursors (F).Last + 1
-                       and Valid_Value (F, Cursors (F).Value)))
+      and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then