From c6c5573f067dd2f02fe9301ae3a7f6b4069930f5 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Wed, 17 Aug 2022 15:36:48 +0200 Subject: [PATCH] Remove unnecessary checking of buffer sizes Ref. #1131 --- rflx/generator/session.py | 125 +++++++++++------- .../generated/rflx-test-session.adb | 36 +---- .../generated/rflx-test-session.adb | 24 +--- .../generated/rflx-test-session.adb | 36 +---- .../generated/rflx-test-session.adb | 43 +----- 5 files changed, 87 insertions(+), 177 deletions(-) diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 78c21ce6d..3b37172b1 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -2212,12 +2212,14 @@ def _assign( # pylint: disable = too-many-arguments return self._assign_to_selected(target, expression, exception_handler, is_global) if isinstance(expression, expr.Head): - return self._assign_to_head(target, expression, exception_handler, is_global, alloc_id) + return self._assign_to_head( + target, expression, exception_handler, is_global, state, alloc_id + ) if isinstance(expression, expr.Comprehension): assert isinstance(target_type, rty.Sequence) return self._assign_to_comprehension( - target, target_type, expression, exception_handler, is_global, alloc_id + target, target_type, expression, exception_handler, is_global, state, alloc_id ) if isinstance(expression, expr.Call): @@ -2536,12 +2538,13 @@ def _assign_to_delta_message_aggregate( ], ] - def _assign_to_head( + def _assign_to_head( # pylint: disable = too-many-arguments self, target: ID, head: expr.Head, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], + state: ID, alloc_id: Optional[Location], ) -> Sequence[Statement]: assert isinstance(head.prefix.type_, (rty.Sequence, rty.Aggregate)) @@ -2556,16 +2559,19 @@ def _assign_to_head( if isinstance(head.prefix, expr.Comprehension): return self._assign_to_head_comprehension( - target, head, exception_handler, is_global, alloc_id + target, head, exception_handler, is_global, state, alloc_id ) - return self._assign_to_head_sequence(target, head, exception_handler, is_global, alloc_id) + return self._assign_to_head_sequence( + target, head, exception_handler, is_global, state, alloc_id + ) - def _assign_to_head_comprehension( # pylint: disable = too-many-locals + def _assign_to_head_comprehension( # pylint: disable = too-many-arguments, too-many-locals self, target: ID, head: expr.Head, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], + state: ID, alloc_id: Optional[Location], ) -> Sequence[Statement]: comprehension = head.prefix @@ -2650,6 +2656,8 @@ def comprehension_statements( message_id = ID(selected.prefix.name) message_type = selected.prefix.type_.identifier message_field = selected.selector + source_buffer_size = self._allocator.get_size(message_id, state) + target_buffer_size = self._allocator.get_size(target, state) return [ self._if_structural_valid_message( @@ -2663,6 +2671,7 @@ def comprehension_statements( sequence_id, sequence_type_id, comprehension_statements, + target_buffer_size < source_buffer_size, exception_handler, is_global, alloc_id, @@ -2679,12 +2688,13 @@ def comprehension_statements( location=comprehension.sequence.location, ) - def _assign_to_head_sequence( # pylint: disable = too-many-locals + def _assign_to_head_sequence( # pylint: disable = too-many-arguments, too-many-locals self, target: ID, head: expr.Head, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], + state: ID, alloc_id: Optional[Location], ) -> Sequence[Statement]: assert isinstance(head.prefix.type_, rty.Sequence) @@ -2740,6 +2750,8 @@ def _assign_to_head_sequence( # pylint: disable = too-many-locals target_buffer = buffer_id("RFLX_Target_" + target) element_context = ID("RFLX_Head_Ctx") copied_sequence_context = context_id(copy_id(sequence_id), is_global) + source_buffer_size = self._allocator.get_size(sequence_id, state) + target_buffer_size = self._allocator.get_size(target, state) def statements(exception_handler: ExceptionHandler) -> list[Statement]: update_context = self._update_context( @@ -2795,6 +2807,7 @@ def statements(exception_handler: ExceptionHandler) -> list[Statement]: target_type, element_context, target_buffer, + target_buffer_size < source_buffer_size, local_exception_handler.copy( [ CallStatement( @@ -2859,6 +2872,7 @@ def _assign_to_comprehension( # pylint: disable = too-many-arguments comprehension: expr.Comprehension, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], + state: ID, alloc_id: Optional[Location], ) -> Sequence[Statement]: # pylint: disable = too-many-locals @@ -2929,6 +2943,8 @@ def statements(local_exception_handler: ExceptionHandler) -> list[Statement]: location=selected.location, ) message_field = selected.selector + source_buffer_size = self._allocator.get_size(message_id, state) + target_buffer_size = self._allocator.get_size(target, state) return [ reset_target, @@ -2957,6 +2973,7 @@ def statements(local_exception_handler: ExceptionHandler) -> list[Statement]: alloc_id, ) ], + target_buffer_size < source_buffer_size, exception_handler, is_global, alloc_id, @@ -4532,7 +4549,8 @@ def _declare_sequence_copy( # pylint: disable = too-many-arguments sequence_type, sequence_context, copy_id(buffer_id(sequence_identifier)), - exception_handler.copy(free_buffer), + target_buffer_is_smaller=False, + exception_handler=exception_handler.copy(free_buffer), ), self._initialize_context( copy_id(sequence_identifier), @@ -4560,6 +4578,7 @@ def _declare_message_field_sequence_copy( # pylint: disable = too-many-argument sequence_identifier: ID, sequence_type: ID, statements: Callable[[ExceptionHandler], Sequence[Statement]], + target_buffer_is_smaller: bool, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], alloc_id: Optional[Location], @@ -4576,6 +4595,7 @@ def _declare_message_field_sequence_copy( # pylint: disable = too-many-argument message_type, context_id(message_identifier, is_global), buffer_id(sequence_identifier), + target_buffer_is_smaller, local_exception_handler, ), self._if_structural_valid_message_field( @@ -4864,7 +4884,8 @@ def _comprehension_assign_element( # pylint: disable = too-many-arguments target_type_id, element_id, buffer_id(target_buffer), - exception_handler, + target_buffer_is_smaller=True, + exception_handler=exception_handler, ), CallStatement( target_type_id * "Initialize", @@ -5137,54 +5158,60 @@ def _copy_to_buffer( type_: ID, source_context: ID, target_buffer: ID, + target_buffer_is_smaller: bool, exception_handler: ExceptionHandler, - ) -> IfStatement: + ) -> Statement: self._session_context.used_types_body.append(const.TYPES_LENGTH) - return IfStatement( + copy = CallStatement( + type_ * "Copy", [ - ( - LessEqual( - Call( - type_ * "Byte_Size", - [Variable(source_context)], - ), - Length(target_buffer), - ), - [ - CallStatement( - type_ * "Copy", - [ - Variable(source_context), - Indexed( - Variable(target_buffer * "all"), - ValueRange( - First(target_buffer), - Add( - First(target_buffer), - Call( - const.TYPES_INDEX, - [ - Add( - Call( - type_ * "Byte_Size", - [Variable(source_context)], - ), - Number(1), - ) - ], - ), - -Number(2), + Variable(source_context), + Indexed( + Variable(target_buffer * "all"), + ValueRange( + First(target_buffer), + Add( + First(target_buffer), + Call( + const.TYPES_INDEX, + [ + Add( + Call( + type_ * "Byte_Size", + [Variable(source_context)], ), - ), - ), - ], + Number(1), + ) + ], + ), + -Number(2), ), - ], - ) + ), + ), ], - exception_handler.execute(), ) + if target_buffer_is_smaller: + return IfStatement( + [ + ( + LessEqual( + Call( + type_ * "Byte_Size", + [Variable(source_context)], + ), + Length(target_buffer), + ), + [ + copy, + ], + ) + ], + exception_handler.execute(), + ) + + return copy + def _convert_type( self, expression: expr.Expr, target_type: rty.Type, expression_type: rty.Type = None ) -> expr.Expr: diff --git a/tests/integration/session_comprehension_head/generated/rflx-test-session.adb b/tests/integration/session_comprehension_head/generated/rflx-test-session.adb index e58497f16..cdd84a970 100644 --- a/tests/integration/session_comprehension_head/generated/rflx-test-session.adb +++ b/tests/integration/session_comprehension_head/generated/rflx-test-session.adb @@ -173,17 +173,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_4 := null; pragma Warnings (On, "unused assignment"); - if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then - Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null); - pragma Assert (RFLX_Copy_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_4 := RFLX_Copy_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); - pragma Assert (Process_1_Invariant); - goto Finalize_Process_1; - end if; + Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx)); declare RFLX_First_Option_Length_Found : Boolean := False; @@ -284,17 +274,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_5 := null; pragma Warnings (On, "unused assignment"); - if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then - Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_5 = null); - pragma Assert (RFLX_Copy_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_5 := RFLX_Copy_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_5 /= null); - pragma Assert (Process_1_Invariant); - goto Finalize_Process_1; - end if; + Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx)); declare RFLX_First_Option_Found : Boolean := False; @@ -496,17 +476,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_4 := null; pragma Warnings (On, "unused assignment"); - if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then - Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null); - pragma Assert (RFLX_Message_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_4 := RFLX_Message_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); - pragma Assert (Process_2_Invariant); - goto Finalize_Process_2; - end if; + Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options)); declare diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.adb b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.adb index b331a1e7b..ef722d53d 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.adb +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.adb @@ -86,17 +86,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_3 := null; pragma Warnings (On, "unused assignment"); - if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then - Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_3 = null); - pragma Assert (RFLX_Message_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_3 := RFLX_Message_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_3 /= null); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; + Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options)); while Universal.Options.Has_Element (RFLX_Message_Options_Ctx) loop @@ -193,17 +183,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_4 := null; pragma Warnings (On, "unused assignment"); - if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then - Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null); - pragma Assert (RFLX_Message_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_4 := RFLX_Message_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; + Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2)); if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options)); while Universal.Options.Has_Element (RFLX_Message_Options_Ctx) loop diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb index a9537da16..505e8d6ad 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb @@ -200,17 +200,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_6 := null; pragma Warnings (On, "unused assignment"); - if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then - Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 = null); - pragma Assert (RFLX_Copy_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_6 := RFLX_Copy_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 /= null); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; + Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx)); Universal.Option_Types.Reset (Option_Types_Ctx); while Universal.Options.Has_Element (RFLX_Copy_Options_Ctx) loop @@ -297,17 +287,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_7 := null; pragma Warnings (On, "unused assignment"); - if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then - Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_7 = null); - pragma Assert (RFLX_Copy_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_7 := RFLX_Copy_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_7 /= null); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; + Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx)); Universal.Option_Types.Reset (Option_Types_Ctx); while Universal.Options.Has_Element (RFLX_Copy_Options_Ctx) loop @@ -421,17 +401,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_8 := null; pragma Warnings (On, "unused assignment"); - if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then - Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_8 = null); - pragma Assert (RFLX_Copy_Options_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_8 := RFLX_Copy_Options_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_8 /= null); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; + Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2)); Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx)); Universal.Options.Reset (Message_Options_Ctx); while Universal.Options.Has_Element (RFLX_Copy_Options_Ctx) loop diff --git a/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb b/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb index c6fa5ee1c..f3da36155 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb +++ b/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb @@ -94,17 +94,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_4 := null; pragma Warnings (On, "unused assignment"); - if TLV.Messages.Byte_Size (Ctx.P.Messages_Ctx) <= RFLX_Copy_Messages_Buffer'Length then - TLV.Messages.Copy (Ctx.P.Messages_Ctx, RFLX_Copy_Messages_Buffer.all (RFLX_Copy_Messages_Buffer'First .. RFLX_Copy_Messages_Buffer'First + RFLX_Types.Index (TLV.Messages.Byte_Size (Ctx.P.Messages_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null); - pragma Assert (RFLX_Copy_Messages_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_4 := RFLX_Copy_Messages_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); - pragma Assert (Global_Invariant); - goto Finalize_Global; - end if; + TLV.Messages.Copy (Ctx.P.Messages_Ctx, RFLX_Copy_Messages_Buffer.all (RFLX_Copy_Messages_Buffer'First .. RFLX_Copy_Messages_Buffer'First + RFLX_Types.Index (TLV.Messages.Byte_Size (Ctx.P.Messages_Ctx) + 1) - 2)); TLV.Messages.Initialize (RFLX_Copy_Messages_Ctx, RFLX_Copy_Messages_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Messages_Buffer'First), TLV.Messages.Sequence_Last (Ctx.P.Messages_Ctx)); if TLV.Messages.Has_Element (RFLX_Copy_Messages_Ctx) then declare @@ -392,17 +382,7 @@ is pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_6 := null; pragma Warnings (On, "unused assignment"); - if TLV.Messages.Byte_Size (Local_Messages_Ctx) <= RFLX_Copy_Local_Messages_Buffer'Length then - TLV.Messages.Copy (Local_Messages_Ctx, RFLX_Copy_Local_Messages_Buffer.all (RFLX_Copy_Local_Messages_Buffer'First .. RFLX_Copy_Local_Messages_Buffer'First + RFLX_Types.Index (TLV.Messages.Byte_Size (Local_Messages_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 = null); - pragma Assert (RFLX_Copy_Local_Messages_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_6 := RFLX_Copy_Local_Messages_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 /= null); - pragma Assert (Local_Invariant); - goto Finalize_Local; - end if; + TLV.Messages.Copy (Local_Messages_Ctx, RFLX_Copy_Local_Messages_Buffer.all (RFLX_Copy_Local_Messages_Buffer'First .. RFLX_Copy_Local_Messages_Buffer'First + RFLX_Types.Index (TLV.Messages.Byte_Size (Local_Messages_Ctx) + 1) - 2)); TLV.Messages.Initialize (RFLX_Copy_Local_Messages_Ctx, RFLX_Copy_Local_Messages_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Local_Messages_Buffer'First), TLV.Messages.Sequence_Last (Local_Messages_Ctx)); if TLV.Messages.Has_Element (RFLX_Copy_Local_Messages_Ctx) then declare @@ -415,24 +395,7 @@ is pragma Warnings (Off, """Ctx.P.Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); TLV.Message.Take_Buffer (Ctx.P.Message_Ctx, RFLX_Target_Message_Buffer); pragma Warnings (On, """Ctx.P.Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); - if TLV.Message.Byte_Size (RFLX_Head_Ctx) <= RFLX_Target_Message_Buffer'Length then - TLV.Message.Copy (RFLX_Head_Ctx, RFLX_Target_Message_Buffer.all (RFLX_Target_Message_Buffer'First .. RFLX_Target_Message_Buffer'First + RFLX_Types.Index (TLV.Message.Byte_Size (RFLX_Head_Ctx) + 1) - 2)); - else - Ctx.P.Next_State := S_Terminated; - TLV.Message.Initialize (Ctx.P.Message_Ctx, RFLX_Target_Message_Buffer); - pragma Warnings (Off, """RFLX_Head_Ctx"" is set by ""Update"" but not used after the call"); - TLV.Messages.Update (RFLX_Copy_Local_Messages_Ctx, RFLX_Head_Ctx); - pragma Warnings (On, """RFLX_Head_Ctx"" is set by ""Update"" but not used after the call"); - pragma Warnings (Off, """RFLX_Copy_Local_Messages_Ctx"" is set by ""Take_Buffer"" but not used after the call"); - TLV.Messages.Take_Buffer (RFLX_Copy_Local_Messages_Ctx, RFLX_Copy_Local_Messages_Buffer); - pragma Warnings (On, """RFLX_Copy_Local_Messages_Ctx"" is set by ""Take_Buffer"" but not used after the call"); - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 = null); - pragma Assert (RFLX_Copy_Local_Messages_Buffer /= null); - Ctx.P.Slots.Slot_Ptr_6 := RFLX_Copy_Local_Messages_Buffer; - pragma Assert (Ctx.P.Slots.Slot_Ptr_6 /= null); - pragma Assert (Local_Invariant); - goto Finalize_Local; - end if; + TLV.Message.Copy (RFLX_Head_Ctx, RFLX_Target_Message_Buffer.all (RFLX_Target_Message_Buffer'First .. RFLX_Target_Message_Buffer'First + RFLX_Types.Index (TLV.Message.Byte_Size (RFLX_Head_Ctx) + 1) - 2)); TLV.Message.Initialize (Ctx.P.Message_Ctx, RFLX_Target_Message_Buffer, TLV.Message.Size (RFLX_Head_Ctx)); TLV.Message.Verify_Message (Ctx.P.Message_Ctx); else