From f06fd427a4ef4cf30e88aece43fbeb15791fe375 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Thu, 16 Jun 2022 10:21:50 +0900 Subject: [PATCH] remove unused preconditions --- rflx/generator/serializer.py | 30 ------------ .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-test-message.ads | 14 +----- .../generated/rflx-test-message.ads | 22 +-------- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-test-definite_message.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-tlv-message.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-universal-message.ads | 47 ++----------------- .../generated/rflx-universal-option.ads | 14 +----- .../generated/rflx-derivation-message.ads | 14 +----- tests/spark/generated/rflx-ethernet-frame.ads | 11 +---- .../generated/rflx-expression-message.ads | 11 +---- .../rflx-fixed_size-simple_message.ads | 11 +---- tests/spark/generated/rflx-icmp-message.ads | 14 +----- tests/spark/generated/rflx-ipv4-option.ads | 14 +----- tests/spark/generated/rflx-ipv4-packet.ads | 25 +--------- .../generated/rflx-sequence-inner_message.ads | 14 +----- .../spark/generated/rflx-sequence-message.ads | 35 ++------------ .../rflx-sequence-messages_message.ads | 11 +---- ...-sequence_size_defined_by_message_size.ads | 11 +---- tests/spark/generated/rflx-tlv-message.ads | 14 +----- tests/spark/generated/rflx-udp-datagram.ads | 14 +----- 56 files changed, 117 insertions(+), 1335 deletions(-) diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py index fb3e566d87..9e72c9788d 100644 --- a/rflx/generator/serializer.py +++ b/rflx/generator/serializer.py @@ -1624,36 +1624,6 @@ def composite_setter_field_condition_precondition( def composite_setter_preconditions(field: Field, size: Expr = None) -> List[Expr]: return [ common.sufficient_space_for_field_condition(Variable(field.affixed_name), size), - Equal( - Mod( - Call( - "Field_First", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Size(const.TYPES_BYTE), - ), - Number(1), - ), - Equal( - Mod( - Call( - "Field_Last", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Size(const.TYPES_BYTE), - ), - Number(0), - ), - Equal( - Mod( - Call( - "Field_Size", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Size(const.TYPES_BYTE), - ), - Number(0), - ), ] def scalar_setter_and_getter_relation( diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/messages/generated/rflx-universal-message.ads +++ b/tests/integration/messages/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/messages/generated/rflx-universal-option.ads +++ b/tests/integration/messages/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads index e537c6d4e4..94f1fa161e 100644 --- a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads +++ b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads @@ -414,9 +414,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -435,10 +432,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -457,9 +451,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data), @@ -484,9 +475,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.ads b/tests/integration/parameterized_messages/generated/rflx-test-message.ads index 8c7add97a0..565dec3fbb 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-message.ads @@ -452,10 +452,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -480,10 +477,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Extension) - and then Available_Space (Ctx, F_Extension) >= Field_Size (Ctx, F_Extension) - and then Field_First (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Extension) >= Field_Size (Ctx, F_Extension), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Extension) @@ -503,9 +497,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data), @@ -535,9 +526,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Extension) and then Available_Space (Ctx, F_Extension) >= Field_Size (Ctx, F_Extension) - and then Field_First (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Extension, Data'Length) and then Available_Space (Ctx, F_Extension) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Extension), @@ -564,9 +552,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), @@ -598,9 +583,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Extension) and then Available_Space (Ctx, F_Extension) >= Field_Size (Ctx, F_Extension) - and then Field_First (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Extension) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Extension, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Extension)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_binding/generated/rflx-universal-message.ads b/tests/integration/session_binding/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_binding/generated/rflx-universal-message.ads +++ b/tests/integration/session_binding/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_binding/generated/rflx-universal-option.ads b/tests/integration/session_binding/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_binding/generated/rflx-universal-option.ads +++ b/tests/integration/session_binding/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_channels/generated/rflx-universal-message.ads b/tests/integration/session_channels/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_channels/generated/rflx-universal-message.ads +++ b/tests/integration/session_channels/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_channels/generated/rflx-universal-option.ads b/tests/integration/session_channels/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_channels/generated/rflx-universal-option.ads +++ b/tests/integration/session_channels/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_conversion/generated/rflx-universal-message.ads b/tests/integration/session_conversion/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-message.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_conversion/generated/rflx-universal-option.ads b/tests/integration/session_conversion/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-option.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_functions/generated/rflx-test-definite_message.ads b/tests/integration/session_functions/generated/rflx-test-definite_message.ads index 0177940391..255ed9d540 100644 --- a/tests/integration/session_functions/generated/rflx-test-definite_message.ads +++ b/tests/integration/session_functions/generated/rflx-test-definite_message.ads @@ -482,9 +482,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -504,10 +501,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -527,9 +521,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data), @@ -556,9 +547,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_functions/generated/rflx-universal-message.ads b/tests/integration/session_functions/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_functions/generated/rflx-universal-message.ads +++ b/tests/integration/session_functions/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_functions/generated/rflx-universal-option.ads b/tests/integration/session_functions/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_functions/generated/rflx-universal-option.ads +++ b/tests/integration/session_functions/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_functions_opaque/generated/rflx-universal-message.ads b/tests/integration/session_functions_opaque/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_functions_opaque/generated/rflx-universal-message.ads +++ b/tests/integration/session_functions_opaque/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_functions_opaque/generated/rflx-universal-option.ads b/tests/integration/session_functions_opaque/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_functions_opaque/generated/rflx-universal-option.ads +++ b/tests/integration/session_functions_opaque/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_integration/generated/rflx-universal-message.ads b/tests/integration/session_integration/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_integration/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_integration/generated/rflx-universal-option.ads b/tests/integration/session_integration/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_integration/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_minimal/generated/rflx-universal-message.ads b/tests/integration/session_minimal/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-message.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_minimal/generated/rflx-universal-option.ads b/tests/integration/session_minimal/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-option.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_sequence_append/generated/rflx-universal-message.ads b/tests/integration/session_sequence_append/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_sequence_append/generated/rflx-universal-message.ads +++ b/tests/integration/session_sequence_append/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_sequence_append/generated/rflx-universal-option.ads b/tests/integration/session_sequence_append/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_sequence_append/generated/rflx-universal-option.ads +++ b/tests/integration/session_sequence_append/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads index 74902c74fd..c0d9cf61c3 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads +++ b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Value) and then Field_Condition (Ctx, F_Value, 0) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Value) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) - and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Value) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Data'Length) and then Available_Space (Ctx, F_Value) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Value, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Value)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_setting_of_message_fields/generated/rflx-universal-message.ads b/tests/integration/session_setting_of_message_fields/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_setting_of_message_fields/generated/rflx-universal-message.ads +++ b/tests/integration/session_setting_of_message_fields/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_setting_of_message_fields/generated/rflx-universal-option.ads b/tests/integration/session_setting_of_message_fields/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_setting_of_message_fields/generated/rflx-universal-option.ads +++ b/tests/integration/session_setting_of_message_fields/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_simple/generated/rflx-universal-message.ads b/tests/integration/session_simple/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_simple/generated/rflx-universal-message.ads +++ b/tests/integration/session_simple/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_simple/generated/rflx-universal-option.ads b/tests/integration/session_simple/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_simple/generated/rflx-universal-option.ads +++ b/tests/integration/session_simple/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads index 05358fb544..65c755ffa0 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads @@ -562,9 +562,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -589,9 +586,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Types) = 0, Post => Has_Buffer (Ctx) @@ -616,9 +610,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -641,9 +632,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Values) = 0, Post => Has_Buffer (Ctx) @@ -665,9 +653,6 @@ is and then Valid_Next (Ctx, F_Option_Types) and then Field_Condition (Ctx, F_Option_Types, 0) and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx)) and then Universal.Option_Types.Has_Buffer (Seq_Ctx) and then Universal.Option_Types.Valid (Seq_Ctx), @@ -695,9 +680,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx)) and then Universal.Options.Has_Buffer (Seq_Ctx) and then Universal.Options.Valid (Seq_Ctx), @@ -723,9 +705,6 @@ is and then Valid_Next (Ctx, F_Values) and then Field_Condition (Ctx, F_Values, 0) and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx)) and then Universal.Values.Has_Buffer (Seq_Ctx) and then Universal.Values.Valid (Seq_Ctx), @@ -749,10 +728,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -775,10 +751,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Types) - and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types) - and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Types) @@ -801,10 +774,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) and then Valid_Length (Ctx, F_Options, Length) - and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -825,10 +795,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Values) - and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values) - and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Values) @@ -848,9 +815,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -880,9 +844,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads index 89fa9059ca..03bf88f985 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index 866020a146..13d0cb3fc7 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -487,9 +487,6 @@ is and then Valid_Next (Ctx, F_Value) and then Field_Condition (Ctx, F_Value, 0) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Value) = 0, Post => Has_Buffer (Ctx) @@ -509,10 +506,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) - and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Value) @@ -532,9 +526,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Data'Length) and then Available_Space (Ctx, F_Value) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Value, 0), @@ -561,9 +552,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Value)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index 6df940d920..26e3bf0f50 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -636,10 +636,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Valid_Length (Ctx, F_Payload, Length) - and then Available_Space (Ctx, F_Payload) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Payload) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Payload) @@ -662,9 +659,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Data'Length) and then Available_Space (Ctx, F_Payload) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Payload, 0, RFLX_Types.To_Bit_Length (Data'Length)), @@ -693,9 +687,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index 1f8147ed16..88baae9a86 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.ads @@ -410,10 +410,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) - and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Payload) @@ -431,9 +428,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Data'Length) and then Available_Space (Ctx, F_Payload) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Payload, Data), @@ -458,9 +452,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 31b3da900f..a6aa82ab53 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -454,10 +454,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) - and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -476,9 +473,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -504,9 +498,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index 4d55aa465c..ca559a91d3 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -1050,9 +1050,6 @@ is and then Valid_Next (Ctx, F_Data) and then Field_Condition (Ctx, F_Data, 0) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Data) = 0, Post => Has_Buffer (Ctx) @@ -1075,10 +1072,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Valid_Length (Ctx, F_Data, Length) - and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Data) @@ -1101,9 +1095,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Data'Length) and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Data, 0), @@ -1132,9 +1123,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Data) and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data) - and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index 909e994548..f35e5e89a5 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -570,9 +570,6 @@ is and then Valid_Next (Ctx, F_Option_Data) and then Field_Condition (Ctx, F_Option_Data, 0) and then Available_Space (Ctx, F_Option_Data) >= Field_Size (Ctx, F_Option_Data) - and then Field_First (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Option_Data) = 0, Post => Has_Buffer (Ctx) @@ -594,10 +591,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Data) - and then Available_Space (Ctx, F_Option_Data) >= Field_Size (Ctx, F_Option_Data) - and then Field_First (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Option_Data) >= Field_Size (Ctx, F_Option_Data), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Option_Data) @@ -619,9 +613,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Data) and then Available_Space (Ctx, F_Option_Data) >= Field_Size (Ctx, F_Option_Data) - and then Field_First (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Data, Data'Length) and then Available_Space (Ctx, F_Option_Data) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Option_Data, 0), @@ -650,9 +641,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Option_Data) and then Available_Space (Ctx, F_Option_Data) >= Field_Size (Ctx, F_Option_Data) - and then Field_First (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Option_Data) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Option_Data, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Option_Data)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index 15d2aafa7c..c81add2f0e 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -1076,9 +1076,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Options) = 0, Post => Has_Buffer (Ctx) @@ -1114,9 +1111,6 @@ is and then Valid_Next (Ctx, F_Payload) and then Field_Condition (Ctx, F_Payload, 0) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Payload) = 0, Post => Has_Buffer (Ctx) @@ -1150,9 +1144,6 @@ is and then Valid_Next (Ctx, F_Options) and then Field_Condition (Ctx, F_Options, 0) and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Options, IPv4.Options.Byte_Size (Seq_Ctx)) and then IPv4.Options.Has_Buffer (Seq_Ctx) and then IPv4.Options.Valid (Seq_Ctx), @@ -1189,10 +1180,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Options) - and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options) - and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Options) @@ -1225,10 +1213,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) - and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Payload) @@ -1260,9 +1245,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Data'Length) and then Available_Space (Ctx, F_Payload) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Payload, 0), @@ -1301,9 +1283,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index 60e6520fa9..455356efbb 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -449,9 +449,6 @@ is and then Valid_Next (Ctx, F_Payload) and then Field_Condition (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Payload) = 0, Post => Has_Buffer (Ctx) @@ -470,10 +467,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) - and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Payload) @@ -492,9 +486,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Data'Length) and then Available_Space (Ctx, F_Payload) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Payload), @@ -520,9 +511,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index 6e4dbfc71e..8ac78fcd39 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -431,9 +431,6 @@ is and then Valid_Next (Ctx, F_Modular_Vector) and then Field_Condition (Ctx, F_Modular_Vector) and then Available_Space (Ctx, F_Modular_Vector) >= Field_Size (Ctx, F_Modular_Vector) - and then Field_First (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Modular_Vector) = 0, Post => Has_Buffer (Ctx) @@ -458,9 +455,6 @@ is and then Valid_Next (Ctx, F_Modular_Vector) and then Field_Condition (Ctx, F_Modular_Vector) and then Available_Space (Ctx, F_Modular_Vector) >= Field_Size (Ctx, F_Modular_Vector) - and then Field_First (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Modular_Vector, Sequence.Modular_Vector.Byte_Size (Seq_Ctx)) and then Sequence.Modular_Vector.Has_Buffer (Seq_Ctx) and then Sequence.Modular_Vector.Valid (Seq_Ctx), @@ -488,9 +482,6 @@ is and then Valid_Next (Ctx, F_Range_Vector) and then Field_Condition (Ctx, F_Range_Vector) and then Available_Space (Ctx, F_Range_Vector) >= Field_Size (Ctx, F_Range_Vector) - and then Field_First (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Range_Vector, Sequence.Range_Vector.Byte_Size (Seq_Ctx)) and then Sequence.Range_Vector.Has_Buffer (Seq_Ctx) and then Sequence.Range_Vector.Valid (Seq_Ctx), @@ -517,9 +508,6 @@ is and then Valid_Next (Ctx, F_Enumeration_Vector) and then Field_Condition (Ctx, F_Enumeration_Vector) and then Available_Space (Ctx, F_Enumeration_Vector) >= Field_Size (Ctx, F_Enumeration_Vector) - and then Field_First (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Enumeration_Vector, Sequence.Enumeration_Vector.Byte_Size (Seq_Ctx)) and then Sequence.Enumeration_Vector.Has_Buffer (Seq_Ctx) and then Sequence.Enumeration_Vector.Valid (Seq_Ctx), @@ -545,9 +533,6 @@ is and then Valid_Next (Ctx, F_AV_Enumeration_Vector) and then Field_Condition (Ctx, F_AV_Enumeration_Vector) and then Available_Space (Ctx, F_AV_Enumeration_Vector) >= Field_Size (Ctx, F_AV_Enumeration_Vector) - and then Field_First (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_AV_Enumeration_Vector, Sequence.AV_Enumeration_Vector.Byte_Size (Seq_Ctx)) and then Sequence.AV_Enumeration_Vector.Has_Buffer (Seq_Ctx) and then Sequence.AV_Enumeration_Vector.Valid (Seq_Ctx), @@ -572,10 +557,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Modular_Vector) - and then Available_Space (Ctx, F_Modular_Vector) >= Field_Size (Ctx, F_Modular_Vector) - and then Field_First (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Modular_Vector) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Modular_Vector) >= Field_Size (Ctx, F_Modular_Vector), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Modular_Vector) @@ -597,10 +579,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Range_Vector) - and then Available_Space (Ctx, F_Range_Vector) >= Field_Size (Ctx, F_Range_Vector) - and then Field_First (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Range_Vector) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Range_Vector) >= Field_Size (Ctx, F_Range_Vector), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Range_Vector) @@ -621,10 +600,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Enumeration_Vector) - and then Available_Space (Ctx, F_Enumeration_Vector) >= Field_Size (Ctx, F_Enumeration_Vector) - and then Field_First (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Enumeration_Vector) >= Field_Size (Ctx, F_Enumeration_Vector), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Enumeration_Vector) @@ -644,10 +620,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_AV_Enumeration_Vector) - and then Available_Space (Ctx, F_AV_Enumeration_Vector) >= Field_Size (Ctx, F_AV_Enumeration_Vector) - and then Field_First (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_AV_Enumeration_Vector) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_AV_Enumeration_Vector) >= Field_Size (Ctx, F_AV_Enumeration_Vector), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_AV_Enumeration_Vector) diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index c4a410394c..680eb951aa 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -425,9 +425,6 @@ is and then Valid_Next (Ctx, F_Messages) and then Field_Condition (Ctx, F_Messages) and then Available_Space (Ctx, F_Messages) >= Field_Size (Ctx, F_Messages) - and then Field_First (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Messages) = 0, Post => Has_Buffer (Ctx) @@ -448,9 +445,6 @@ is and then Valid_Next (Ctx, F_Messages) and then Field_Condition (Ctx, F_Messages) and then Available_Space (Ctx, F_Messages) >= Field_Size (Ctx, F_Messages) - and then Field_First (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Messages, Sequence.Inner_Messages.Byte_Size (Seq_Ctx)) and then Sequence.Inner_Messages.Has_Buffer (Seq_Ctx) and then Sequence.Inner_Messages.Valid (Seq_Ctx), @@ -472,10 +466,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Messages) - and then Available_Space (Ctx, F_Messages) >= Field_Size (Ctx, F_Messages) - and then Field_First (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Messages) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Messages) >= Field_Size (Ctx, F_Messages), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Messages) 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 3a82e0ced6..58736f3cf6 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 @@ -425,9 +425,6 @@ is and then Valid_Next (Ctx, F_Vector) and then Field_Condition (Ctx, F_Vector) and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector) - and then Field_First (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Vector) = 0, Post => Has_Buffer (Ctx) @@ -448,9 +445,6 @@ is and then Valid_Next (Ctx, F_Vector) and then Field_Condition (Ctx, F_Vector) and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector) - and then Field_First (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Vector, Sequence.Modular_Vector.Byte_Size (Seq_Ctx)) and then Sequence.Modular_Vector.Has_Buffer (Seq_Ctx) and then Sequence.Modular_Vector.Valid (Seq_Ctx), @@ -473,10 +467,7 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Vector) and then Valid_Length (Ctx, F_Vector, Length) - and then Available_Space (Ctx, F_Vector) >= RFLX_Types.To_Bit_Length (Length) - and then Field_First (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Vector) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Vector) >= RFLX_Types.To_Bit_Length (Length), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Vector) diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index 74902c74fd..c0d9cf61c3 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/generated/rflx-tlv-message.ads @@ -485,9 +485,6 @@ is and then Valid_Next (Ctx, F_Value) and then Field_Condition (Ctx, F_Value, 0) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Value) = 0, Post => Has_Buffer (Ctx) @@ -507,10 +504,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) - and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Value) @@ -530,9 +524,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Data'Length) and then Available_Space (Ctx, F_Value) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Value, 0), @@ -559,9 +550,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Value) and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value) - and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Value, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Value)) >= Length and then Process_Data_Pre (Length), diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index da1a78fa7d..b57e44d5e4 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -548,9 +548,6 @@ is and then Valid_Next (Ctx, F_Payload) and then Field_Condition (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Field_Size (Ctx, F_Payload) = 0, Post => Has_Buffer (Ctx) @@ -572,10 +569,7 @@ is not Ctx'Constrained and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) - and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0, + and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload), Post => Has_Buffer (Ctx) and Structural_Valid (Ctx, F_Payload) @@ -597,9 +591,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Data'Length) and then Available_Space (Ctx, F_Payload) >= Data'Length * RFLX_Types.Byte'Size and then Field_Condition (Ctx, F_Payload), @@ -628,9 +619,6 @@ is and then Has_Buffer (Ctx) and then Valid_Next (Ctx, F_Payload) and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload) - and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1 - and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 - and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0 and then Valid_Length (Ctx, F_Payload, Length) and then RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length and then Process_Data_Pre (Length),