From 0d3836cc2a35249650e75e991bfdfa900008b192 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Tue, 10 May 2022 17:43:44 +0200 Subject: [PATCH] Fix size determination of write buffer Ref. #895 --- rflx/generator/session.py | 47 +++++++++++++++---- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 21 +++++++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 15 ++++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-b-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../generated/rflx-test-session.ads | 13 +++-- .../specification_model_generator_test.py | 39 +++++++++++++++ 20 files changed, 267 insertions(+), 63 deletions(-) diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 71fe6bf634..9ddea0ce9e 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -386,7 +386,7 @@ def is_global(identifier: ID) -> bool: if has_reads: unit += self._create_needs_data_function(channel_reads) - unit += self._create_write_buffer_size_function(channel_reads) + unit += self._create_write_buffer_size_function(channel_reads, is_global) unit += self._create_write_procedure(channel_reads, is_global) return ( @@ -1397,17 +1397,31 @@ def _create_read_buffer_size_function( @staticmethod def _create_write_buffer_size_function( - channel_reads: dict[rid.ID, list[ChannelAccess]] + channel_reads: dict[rid.ID, list[ChannelAccess]], + is_global: Callable[[ID], bool], ) -> UnitPart: specification = FunctionSpecification( "Write_Buffer_Size", const.TYPES_LENGTH, - [Parameter(["Unused_Ctx"], "Context'Class"), Parameter(["Chan"], "Channel")], + [ + Parameter(["Ctx"], "Context'Class"), + Parameter(["Chan"], "Channel"), + ], ) return UnitPart( [ - SubprogramDeclaration(specification), + SubprogramDeclaration( + specification, + [ + Precondition( + AndThen( + Call("Initialized", [Variable("Ctx")]), + Call("Needs_Data", [Variable("Ctx"), Variable("Chan")]), + ) + ), + ], + ), ], private=[ ExpressionFunctionDeclaration( @@ -1415,10 +1429,27 @@ def _create_write_buffer_size_function( Case( Variable("Chan"), [ - # ISSUE: Componolit/RecordFlux#895 - # Size of correspondig buffer must be returned instead of constant - # value. - (Variable(f"C_{channel}"), Number(4096) if reads else Number(0)) + ( + Variable(f"C_{channel}"), + Case( + Variable("Ctx.P.Next_State"), + [ + *[ + ( + Variable(f"S_{read.state}"), + Call( + read.message_type * "Buffer_Length", + [Variable(context_id(read.message, is_global))], + ), + ) + for read in reads + ], + (Variable("others"), const.UNREACHABLE), + ], + ) + if reads + else Number(0), + ) for channel, reads in channel_reads.items() ], ), diff --git a/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads b/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads index ceea4e5a1e..e154f294ff 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -164,9 +167,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.M_R_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads index 949a7b65e7..0e8fb61961 100644 --- a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads +++ b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads @@ -89,7 +89,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -163,9 +166,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Test.Message.Buffer_Length (Ctx.P.M_R_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session.ads b/tests/integration/parameterized_messages/generated/rflx-test-session.ads index bafa67ae85..b7b7d73c80 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-session.ads @@ -89,7 +89,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -163,9 +166,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_C => - 4096)); + (case Ctx.P.Next_State is + when S_Receive => + Test.Message.Buffer_Length (Ctx.P.M_R_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_binding/generated/rflx-test-session.ads b/tests/integration/session_binding/generated/rflx-test-session.ads index 8ec0078b68..4712bfc625 100644 --- a/tests/integration/session_binding/generated/rflx-test-session.ads +++ b/tests/integration/session_binding/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads b/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads index 2eb2af9e14..0172872ed7 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -175,10 +178,20 @@ private when C_O => False)); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is - when C_I_1 | C_I_2 => - 4096, + when C_I_1 => + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_1_Ctx), + when others => + RFLX_Types.Unreachable), + when C_I_2 => + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_2_Ctx), + when others => + RFLX_Types.Unreachable), when C_O => 0)); diff --git a/tests/integration/session_channels/generated/rflx-test-session.ads b/tests/integration/session_channels/generated/rflx-test-session.ads index 98848488cc..74b8d26737 100644 --- a/tests/integration/session_channels/generated/rflx-test-session.ads +++ b/tests/integration/session_channels/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -165,10 +168,14 @@ private when C_O => False)); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_I => - 4096, + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable), when C_O => 0)); diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads index 8ec0078b68..4712bfc625 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_conversion/generated/rflx-test-session.ads b/tests/integration/session_conversion/generated/rflx-test-session.ads index 71860eea02..00f8570a97 100644 --- a/tests/integration/session_conversion/generated/rflx-test-session.ads +++ b/tests/integration/session_conversion/generated/rflx-test-session.ads @@ -91,7 +91,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -165,9 +168,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_endianness/generated/rflx-test-session.ads b/tests/integration/session_endianness/generated/rflx-test-session.ads index ca61ceadb5..b8c8eb97b0 100644 --- a/tests/integration/session_endianness/generated/rflx-test-session.ads +++ b/tests/integration/session_endianness/generated/rflx-test-session.ads @@ -92,7 +92,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -187,10 +190,16 @@ private when C_O => False)); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_I => - 4096, + (case Ctx.P.Next_State is + when S_Start => + Messages.Msg_LE_Nested.Buffer_Length (Ctx.P.In_Msg_Ctx), + when S_Read2 => + Messages.Msg_LE.Buffer_Length (Ctx.P.In_Msg2_Ctx), + when others => + RFLX_Types.Unreachable), when C_O => 0)); diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads index 226047e0da..18f6299755 100644 --- a/tests/integration/session_functions/generated/rflx-test-session.ads +++ b/tests/integration/session_functions/generated/rflx-test-session.ads @@ -110,7 +110,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -184,9 +187,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_integration/generated/rflx-test-session.ads b/tests/integration/session_integration/generated/rflx-test-session.ads index 66174c9b65..0fc119e12e 100644 --- a/tests/integration/session_integration/generated/rflx-test-session.ads +++ b/tests/integration/session_integration/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_integration_multiple/generated/rflx-b-session.ads b/tests/integration/session_integration_multiple/generated/rflx-b-session.ads index bf16f58110..1ea9b566af 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-b-session.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-b-session.ads @@ -71,7 +71,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -121,9 +124,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.M_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.B.Session; diff --git a/tests/integration/session_integration_multiple/generated/rflx-test-session.ads b/tests/integration/session_integration_multiple/generated/rflx-test-session.ads index 3ed4aa93a5..749fb9f3d8 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-test-session.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-test-session.ads @@ -71,7 +71,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -121,9 +124,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.M_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_minimal/generated/rflx-test-session.ads b/tests/integration/session_minimal/generated/rflx-test-session.ads index 8c8dda5480..7993fdf6ce 100644 --- a/tests/integration/session_minimal/generated/rflx-test-session.ads +++ b/tests/integration/session_minimal/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_reuse_of_message/generated/rflx-test-session.ads b/tests/integration/session_reuse_of_message/generated/rflx-test-session.ads index 8c8dda5480..7993fdf6ce 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-test-session.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_sequence_append/generated/rflx-test-session.ads b/tests/integration/session_sequence_append/generated/rflx-test-session.ads index 263d651a1e..0291cf6567 100644 --- a/tests/integration/session_sequence_append/generated/rflx-test-session.ads +++ b/tests/integration/session_sequence_append/generated/rflx-test-session.ads @@ -91,7 +91,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -165,9 +168,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Option.Buffer_Length (Ctx.P.Option_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_simple/generated/rflx-test-session.ads b/tests/integration/session_simple/generated/rflx-test-session.ads index 8ec0078b68..4712bfc625 100644 --- a/tests/integration/session_simple/generated/rflx-test-session.ads +++ b/tests/integration/session_simple/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -159,9 +162,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/session_variable_initialization/generated/rflx-test-session.ads b/tests/integration/session_variable_initialization/generated/rflx-test-session.ads index c17f8d541a..6a63a40efd 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-test-session.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-test-session.ads @@ -90,7 +90,10 @@ is Pre => Initialized (Ctx); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length; + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with + Pre => + Initialized (Ctx) + and then Needs_Data (Ctx, Chan); procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with Pre => @@ -161,9 +164,13 @@ private when others => False))); - function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is + function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is ((case Chan is when C_Channel => - 4096)); + (case Ctx.P.Next_State is + when S_Start => + Universal.Message.Buffer_Length (Ctx.P.Message_Ctx), + when others => + RFLX_Types.Unreachable))); end RFLX.Test.Session; diff --git a/tests/integration/specification_model_generator_test.py b/tests/integration/specification_model_generator_test.py index 3fda610bcf..441ff61625 100644 --- a/tests/integration/specification_model_generator_test.py +++ b/tests/integration/specification_model_generator_test.py @@ -747,3 +747,42 @@ def test_session_move_content_of_opaque_field(tmp_path: Path) -> None: end Test; """ utils.assert_compilable_code_string(spec, tmp_path) + + +@pytest.mark.parametrize( + "mode, action", + [ + ("Readable", "Read"), + ("Writable", "Write"), + ], +) +def test_session_single_channel(mode: str, action: str, tmp_path: Path) -> None: + spec = f""" + package Test is + + type Message is + message + Data : Opaque; + end message; + + generic + Channel : Channel with {mode}; + session Session with + Initial => Init, + Final => Terminated + is + Message : Message; + begin + state Init is + begin + Channel'{action} (Message); + transition + goto Terminated + end Init; + + state Terminated is null state; + end Session; + + end Test; + """ + utils.assert_compilable_code_string(spec, tmp_path)