From e3919958ed3eb6dbcad232d0168073514cba0e60 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Wed, 23 Aug 2023 08:56:12 +0900 Subject: [PATCH] generated code --- .../generated/rflx-test-message.ads | 26 +++++++++++++------ .../generated/rflx-test-message.ads | 26 +++++++++++++------ .../generated/rflx-test-message.ads | 26 +++++++++++++------ .../generated/rflx-messages-msg.ads | 26 +++++++++++++------ .../generated/rflx-messages-msg_le.ads | 26 +++++++++++++------ .../generated/rflx-messages-msg_le_nested.ads | 26 +++++++++++++------ .../generated/rflx-test-definite_message.ads | 26 +++++++++++++------ .../generated/rflx-test-option_data.ads | 26 +++++++++++++------ .../generated/rflx-tlv-message.ads | 26 +++++++++++++------ .../generated/rflx-universal-message.ads | 26 +++++++++++++------ .../generated/rflx-universal-option.ads | 26 +++++++++++++------ .../generated/rflx-derivation-message.ads | 26 +++++++++++++------ .../generated/rflx-enumeration-message.ads | 26 +++++++++++++------ tests/spark/generated/rflx-ethernet-frame.ads | 26 +++++++++++++------ .../generated/rflx-expression-message.ads | 26 +++++++++++++------ .../rflx-fixed_size-simple_message.ads | 26 +++++++++++++------ tests/spark/generated/rflx-icmp-message.ads | 26 +++++++++++++------ tests/spark/generated/rflx-ipv4-option.ads | 26 +++++++++++++------ tests/spark/generated/rflx-ipv4-packet.ads | 26 +++++++++++++------ .../generated/rflx-sequence-inner_message.ads | 26 +++++++++++++------ .../spark/generated/rflx-sequence-message.ads | 26 +++++++++++++------ .../rflx-sequence-messages_message.ads | 26 +++++++++++++------ ...-sequence_size_defined_by_message_size.ads | 26 +++++++++++++------ tests/spark/generated/rflx-tlv-message.ads | 26 +++++++++++++------ tests/spark/generated/rflx-udp-datagram.ads | 26 +++++++++++++------ 25 files changed, 450 insertions(+), 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 index 6589b7db5..03b4765f2 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 @@ -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 index a512fd5a1..d9d15e333 100644 --- 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 index b15be3767..9de640089 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 @@ -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 index 76ea3233c..af77a156b 100644 --- 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 index e7ee8ab3e..1a7bf7111 100644 --- 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 index 01f7996bb..96dfa00f4 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 @@ -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 index 98e627fbd..b91c6172e 100644 --- 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 index f2e9f699a..f5606ccb5 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 @@ -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 index 9dec20e22..500196470 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 @@ -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 index e6bfbaa06..6e324d05e 100644 --- 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 diff --git a/tests/feature/shared/generated/rflx-universal-option.ads b/tests/feature/shared/generated/rflx-universal-option.ads index a592bfd5b..073665fdd 100644 --- a/tests/feature/shared/generated/rflx-universal-option.ads +++ b/tests/feature/shared/generated/rflx-universal-option.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/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index 5cc19ca22..f9d93a5a4 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -629,6 +629,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"); @@ -650,14 +667,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/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads index bece7ca6e..663888a87 100644 --- a/tests/spark/generated/rflx-enumeration-message.ads +++ b/tests/spark/generated/rflx-enumeration-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/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index 90b1f5c89..7e6973a7d 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -769,6 +769,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"); @@ -790,14 +807,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_Source)) then diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index bb0a969ff..c527a5804 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.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 (True) and then (True) and then ((if diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 3353d2b9a..b2a2d1bd9 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -608,6 +608,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"); @@ -629,14 +646,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/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index cf13fca2f..61200b9fb 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -1215,6 +1215,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"); @@ -1236,14 +1253,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_Code_Destination_Unreachable)) then diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index a9fd18cc2..f6080bd1a 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -722,6 +722,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"); @@ -743,14 +760,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_Option_Class)) then diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index c948147bc..05cdc4742 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -1476,6 +1476,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"); @@ -1497,14 +1514,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_IHL)) then diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index 79a75fbd0..81a932aa2 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -623,6 +623,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"); @@ -644,14 +661,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_Payload)) then diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index 4c9f14449..600d2d4d5 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -864,6 +864,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"); @@ -885,14 +902,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_Integer_Vector)) then diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index fa3acbb9c..e653123ff 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -607,6 +607,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"); @@ -628,14 +645,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_Messages)) then 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 bfce31304..0db564113 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 @@ -609,6 +609,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"); @@ -630,14 +647,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_Vector)) then diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index 9dec20e22..500196470 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/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/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index 8a2aeca2d..9004a3cd6 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -752,6 +752,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"); @@ -773,14 +790,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_Destination_Port)) then