diff --git a/rflx/generator/allocator.py b/rflx/generator/allocator.py index 7c15c02b3..55b7c40d6 100644 --- a/rflx/generator/allocator.py +++ b/rflx/generator/allocator.py @@ -126,7 +126,7 @@ def get_slot_ptr(self, location: Optional[Location]) -> ID: slot_id: int = self._allocation_slots[location] return self._slot_name(slot_id) - def get_size(self, variable: rid.ID, state: Optional[rid.ID] = None) -> int: + def get_size(self, variable: Optional[rid.ID] = None, state: Optional[rid.ID] = None) -> int: return self._integration.get_size(self._session.identifier, variable, state) @staticmethod diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 32e7c125a..2ca4f43c4 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -2703,7 +2703,7 @@ def _assign_to_call( # pylint: disable = too-many-locals exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], ) -> Sequence[Statement]: - pre_call = [] + pre_call: list[Statement] = [] post_call = [] local_declarations = [] target_id = variable_id(target, is_global) @@ -2793,7 +2793,7 @@ def _assign_to_call( # pylint: disable = too-many-locals First(const.TYPES_INDEX), Add( First(const.TYPES_INDEX), - Number(4095), + Number(self._allocator.get_size() - 1), ), ), NamedAggregate(("others", Number(0))), @@ -2832,6 +2832,85 @@ def _assign_to_call( # pylint: disable = too-many-locals ), ) arguments.append(argument) + elif ( + isinstance(a, expr.Opaque) + and isinstance(a.prefix, expr.Variable) + and isinstance(a.prefix.type_, rty.Message) + ): + argument_name = f"RFLX_{call_expr.identifier}_Arg_{i}_{a.prefix}" + argument_length = f"{argument_name}_Length" + argument = expr.Slice( + expr.Variable(argument_name), + expr.First(const.TYPES_INDEX), + expr.Add( + expr.First(const.TYPES_INDEX), + expr.Call( + const.TYPES_INDEX, + [expr.Add(expr.Variable(argument_length), expr.Number(1))], + ), + -expr.Number(2), + ), + ) + type_identifier = self._ada_type(a.prefix.type_.identifier) + message_context = context_id(a.prefix.identifier, is_global) + local_declarations.extend( + [ + # ISSUE: Componolit/RecordFlux#917 + # The use of intermediate buffers should be removed. + ObjectDeclaration( + [argument_name], + Slice( + Variable(const.TYPES_BYTES), + First(const.TYPES_INDEX), + Add( + First(const.TYPES_INDEX), + Number(self._allocator.get_size() - 1), + ), + ), + NamedAggregate(("others", Number(0))), + ), + ObjectDeclaration( + [argument_length], + const.TYPES_LENGTH, + Call( + type_identifier * "Byte_Size", + [ + Variable(message_context), + ], + ), + constant=True, + ), + ] + ) + pre_call.extend( + [ + self._raise_exception_if( + Not( + Call( + type_identifier * "Structural_Valid_Message", + [Variable(message_context)], + ) + ), + f'invalid message "{message_context}"', + exception_handler, + ), + CallStatement( + type_identifier * "Message_Data", + [ + Variable(message_context), + argument.ada_expr(), + ], + ), + ] + ) + arguments.append(argument) + elif ( + isinstance(a, expr.Variable) + and isinstance(a.type_, rty.Enumeration) + and a.type_.always_valid + and a.identifier in self._session.literals + ): + arguments.append(expr.NamedAggregate(("Known", expr.TRUE), ("Enum", a))) else: arguments.append(a) @@ -3542,6 +3621,24 @@ def _ensure( ) return nested + def _raise_exception_if( + self, + condition: Expr, + error_message: str, + exception_handler: ExceptionHandler, + ) -> IfStatement: + return IfStatement( + [ + ( + condition, + [ + *self._debug_output(f"Error: {error_message}"), + *exception_handler.execute(), + ], + ), + ] + ) + @staticmethod def _exit_on_deferred_exception() -> ExitStatement: return ExitStatement(Variable("RFLX_Exception")) diff --git a/rflx/integration.py b/rflx/integration.py index a8ffe110d..b3faac401 100644 --- a/rflx/integration.py +++ b/rflx/integration.py @@ -87,14 +87,15 @@ def validate(self, model: Model, error: RecordFluxError) -> None: self._validate_globals(package, integration, session, error) self._validate_states(package, integration, session, error) - def get_size(self, session: ID, variable: ID, state: Optional[ID]) -> int: + def get_size(self, session: ID, variable: Optional[ID], state: Optional[ID]) -> int: """ Return the requested buffer size for a variable of a given session and state. - If state is None, the variable is assumed to be a global - variable. If no specific buffer size was requested for the variable, - return the default buffer size for the session, if present, or the - default buffer size for RecordFlux. + If state is None, the variable is assumed to be a global variable. If variable is None or no + specific buffer size was requested for the variable, return the default buffer size for the + session, if present, or the default buffer size for RecordFlux. + + The returned size is in bytes. """ integration_package = str(session.parent).lower() if integration_package not in self._packages: @@ -105,8 +106,12 @@ def get_size(self, session: ID, variable: ID, state: Optional[ID]) -> int: return self.defaultsize buffer_size = self._packages[integration_package].session[session_name].buffer_size - variable_name = str(variable.name) default_size = self.defaultsize if buffer_size.default is None else buffer_size.default + + if variable is None: + return default_size + + variable_name = str(variable.name) if state is None: if buffer_size.global_ is not None and variable_name in buffer_size.global_: return buffer_size.global_[variable_name] diff --git a/rflx/model/session.py b/rflx/model/session.py index 4bf9c9ead..cd19f408c 100644 --- a/rflx/model/session.py +++ b/rflx/model/session.py @@ -1,3 +1,5 @@ +from __future__ import annotations + import itertools from abc import abstractmethod from collections import defaultdict @@ -200,6 +202,10 @@ def __str__(self) -> str: f"is\n{indent(declarations, 3)}begin\n{indent(states, 3)}\nend {self.identifier.name}" ) + @property + def literals(self) -> Mapping[ID, mty.Type]: + return self._literals + def _resolve_function_calls(self) -> None: """ Replace variables by function calls where necessary. diff --git a/tests/integration/session_functions/config.yml b/tests/integration/session_functions/config.yml index 428d5a137..321b5f9cf 100644 --- a/tests/integration/session_functions/config.yml +++ b/tests/integration/session_functions/config.yml @@ -7,6 +7,10 @@ sequence: | Write Channel: 1 0 3 0 1 2 State: Start State: Process - Read Channel: 1 0 1 2 + Read Channel: 1 3 0 1 2 State: Reply -prove: + State: Process_2 + Read Channel: 1 6 1 0 3 0 1 2 + State: Reply_2 +# ISSUE: Componolit/RecordFlux#691 +# prove: diff --git a/tests/integration/session_functions/fixed_size.rflx b/tests/integration/session_functions/fixed_size.rflx deleted file mode 100644 index d58e1a380..000000000 --- a/tests/integration/session_functions/fixed_size.rflx +++ /dev/null @@ -1,13 +0,0 @@ -with Universal; - -package Fixed_Size is - - type Simple_Message is - message - Message_Type : Universal::Option_Type - then Data - with Size => 24; - Data : Opaque; - end message; - -end Fixed_Size; diff --git a/tests/integration/session_functions/generated/rflx-fixed_size.ads b/tests/integration/session_functions/generated/rflx-fixed_size.ads deleted file mode 100644 index 9e2ec334b..000000000 --- a/tests/integration/session_functions/generated/rflx-fixed_size.ads +++ /dev/null @@ -1,8 +0,0 @@ -pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); -pragma Warnings (Off, "redundant conversion"); - -package RFLX.Fixed_Size with - SPARK_Mode -is - -end RFLX.Fixed_Size; diff --git a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.adb b/tests/integration/session_functions/generated/rflx-test-definite_message.adb similarity index 91% rename from tests/integration/session_functions/generated/rflx-fixed_size-simple_message.adb rename to tests/integration/session_functions/generated/rflx-test-definite_message.adb index 33df24c97..648768448 100644 --- a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.adb +++ b/tests/integration/session_functions/generated/rflx-test-definite_message.adb @@ -1,7 +1,7 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); -package body RFLX.Fixed_Size.Simple_Message with +package body RFLX.Test.Definite_Message with SPARK_Mode is @@ -83,6 +83,8 @@ is function Successor (Ctx : Context; Fld : Field) return Virtual_Field is ((case Fld is when F_Message_Type => + F_Length, + when F_Length => F_Data, when F_Data => F_Final)) @@ -97,6 +99,8 @@ is function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Message_Type => + Invalid (Ctx.Cursors (F_Length)), + when F_Length => Invalid (Ctx.Cursors (F_Data)), when F_Data => True)); @@ -174,7 +178,7 @@ is Buffer_Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Last); Offset : constant RFLX_Types.Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size); Size : constant Positive := (case Fld is - when F_Message_Type => + when F_Message_Type | F_Length => 8, when others => Positive'Last); @@ -276,7 +280,11 @@ is and then (case Fld is when F_Message_Type => Get_Message_Type (Ctx) = To_Actual (Val) - and (Predecessor (Ctx, F_Data) = F_Message_Type + and (Predecessor (Ctx, F_Length) = F_Message_Type + and Valid_Next (Ctx, F_Length)), + when F_Length => + Get_Length (Ctx) = To_Actual (Val) + and (Predecessor (Ctx, F_Data) = F_Length and Valid_Next (Ctx, F_Data)), when F_Data => (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld))) @@ -297,10 +305,10 @@ is Ctx := Ctx'Update (Verified_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size, Written_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size); pragma Warnings (On, "attribute Update is an obsolescent feature"); pragma Assert (Size = (case Fld is - when F_Message_Type => + when F_Message_Type | F_Length => 8, when F_Data => - 24)); + RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8)); if State_Valid then Ctx.Cursors (Fld) := (State => S_Valid, First => First, Last => Last, Value => Val, Predecessor => Ctx.Cursors (Fld).Predecessor); else @@ -318,6 +326,15 @@ is RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First); end Set_Message_Type; + procedure Set_Length (Ctx : in out Context; Val : RFLX.Test.Length) is + Value : constant RFLX_Types.U64 := To_U64 (Val); + Buffer_First, Buffer_Last : RFLX_Types.Index; + Offset : RFLX_Types.Offset; + begin + Set (Ctx, F_Length, Value, 8, True, Buffer_First, Buffer_Last, Offset); + RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First); + end Set_Length; + procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type) with Pre => not Ctx'Constrained @@ -330,9 +347,10 @@ is Has_Buffer (Ctx) and Valid (Ctx, F_Message_Type) and Get_Message_Type (Ctx) = Val + and Invalid (Ctx, F_Length) and Invalid (Ctx, F_Data) - and (Predecessor (Ctx, F_Data) = F_Message_Type - and Valid_Next (Ctx, F_Data)) + and (Predecessor (Ctx, F_Length) = F_Message_Type + and Valid_Next (Ctx, F_Length)) and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old @@ -348,6 +366,13 @@ is RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First); end Set_Message_Type; + procedure Set_Data_Empty (Ctx : in out Context) is + Unused_Buffer_First, Unused_Buffer_Last : RFLX_Types.Index; + Unused_Offset : RFLX_Types.Offset; + begin + Set (Ctx, F_Data, 0, 0, True, Unused_Buffer_First, Unused_Buffer_Last, Unused_Offset); + end Set_Data_Empty; + procedure Initialize_Data_Private (Ctx : in out Context; Length : RFLX_Types.Length) with Pre => not Ctx'Constrained @@ -368,6 +393,7 @@ is and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and Get_Length (Ctx) = Get_Length (Ctx)'Old is First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data); Last : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data) + RFLX_Types.Bit_Length (Length) * RFLX_Types.Byte'Size - 1; @@ -408,6 +434,7 @@ is procedure To_Structure (Ctx : Context; Struct : out Structure) is begin Struct.Message_Type := Get_Message_Type (Ctx); + Struct.Length := Get_Length (Ctx); Struct.Data := (others => 0); Get_Data (Ctx, Struct.Data (Struct.Data'First .. Struct.Data'First + RFLX_Types.Index (RFLX_Types.To_Length (Field_Size (Ctx, F_Data)) + 1) - 2)); end To_Structure; @@ -416,7 +443,8 @@ is begin Reset (Ctx); Set_Message_Type (Ctx, Struct.Message_Type); - Set_Data (Ctx, Struct.Data); + Set_Length (Ctx, Struct.Length); + Set_Data (Ctx, Struct.Data (Struct.Data'First .. Struct.Data'First + RFLX_Types.Index (RFLX_Types.To_Length (RFLX_Types.Bit_Length (Struct.Length) * 8) + 1) - 2)); end To_Context; -end RFLX.Fixed_Size.Simple_Message; +end RFLX.Test.Definite_Message; diff --git a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads b/tests/integration/session_functions/generated/rflx-test-definite_message.ads similarity index 85% rename from tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads rename to tests/integration/session_functions/generated/rflx-test-definite_message.ads index 64cbde326..6dd21aa55 100644 --- a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads +++ b/tests/integration/session_functions/generated/rflx-test-definite_message.ads @@ -4,7 +4,7 @@ with RFLX.RFLX_Types; with RFLX.Universal; use RFLX.Universal; -package RFLX.Fixed_Size.Simple_Message with +package RFLX.Test.Definite_Message with SPARK_Mode, Annotate => (GNATprove, Terminating) @@ -38,7 +38,7 @@ is pragma Unevaluated_Use_Of_Old (Allow); - type Virtual_Field is (F_Initial, F_Message_Type, F_Data, F_Final); + type Virtual_Field is (F_Initial, F_Message_Type, F_Length, F_Data, F_Final); subtype Field is Virtual_Field range F_Message_Type .. F_Data; @@ -382,6 +382,10 @@ is Pre => Valid (Ctx, F_Message_Type); + function Get_Length (Ctx : Context) return RFLX.Test.Length with + Pre => + Valid (Ctx, F_Length); + pragma Warnings (On, "precondition is always False"); function Get_Data (Ctx : Context) return RFLX_Types.Bytes with @@ -431,9 +435,10 @@ is Has_Buffer (Ctx) and Valid (Ctx, F_Message_Type) and Get_Message_Type (Ctx) = (True, Val) + and Invalid (Ctx, F_Length) and Invalid (Ctx, F_Data) - and (Predecessor (Ctx, F_Data) = F_Message_Type - and Valid_Next (Ctx, F_Data)) + and (Predecessor (Ctx, F_Length) = F_Message_Type + and Valid_Next (Ctx, F_Length)) and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old @@ -441,6 +446,55 @@ is and Predecessor (Ctx, F_Message_Type) = Predecessor (Ctx, F_Message_Type)'Old and Valid_Next (Ctx, F_Message_Type) = Valid_Next (Ctx, F_Message_Type)'Old; + procedure Set_Length (Ctx : in out Context; Val : RFLX.Test.Length) with + Pre => + not Ctx'Constrained + and then Has_Buffer (Ctx) + and then Valid_Next (Ctx, F_Length) + and then RFLX.Test.Valid_Length (To_U64 (Val)) + and then Field_Condition (Ctx, F_Length) + and then Available_Space (Ctx, F_Length) >= Field_Size (Ctx, F_Length), + Post => + Has_Buffer (Ctx) + and Valid (Ctx, F_Length) + and Get_Length (Ctx) = Val + and Invalid (Ctx, F_Data) + and (Predecessor (Ctx, F_Data) = F_Length + and Valid_Next (Ctx, F_Data)) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old + and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old + and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and (for all F in Field range F_Message_Type .. F_Message_Type => + Context_Cursors_Index (Context_Cursors (Ctx), F) = Context_Cursors_Index (Context_Cursors (Ctx)'Old, F)); + + procedure Set_Data_Empty (Ctx : in out Context) with + Pre => + not Ctx'Constrained + and then Has_Buffer (Ctx) + 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) + and Structural_Valid (Ctx, F_Data) + and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data)) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old + and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old + and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and Get_Length (Ctx) = Get_Length (Ctx)'Old; + procedure Initialize_Data (Ctx : in out Context) with Pre => not Ctx'Constrained @@ -460,7 +514,8 @@ is and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old - and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old; + and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and Get_Length (Ctx) = Get_Length (Ctx)'Old; procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) with Pre => @@ -485,6 +540,7 @@ is and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and Get_Length (Ctx) = Get_Length (Ctx)'Old and Equal (Ctx, F_Data, Data); generic @@ -512,7 +568,8 @@ is and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old - and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old; + and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old + and Get_Length (Ctx) = Get_Length (Ctx)'Old; function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor with Annotate => @@ -532,7 +589,8 @@ is type Structure is record Message_Type : RFLX.Universal.Option_Type; - Data : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 2); + Length : RFLX.Test.Length; + Data : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 254); end record; function Valid_Structure (Struct : Structure) return Boolean; @@ -549,7 +607,7 @@ is Valid_Structure (Struct) and then not Ctx'Constrained and then Has_Buffer (Ctx) - and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 32, + and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 2056, Post => Has_Buffer (Ctx) and Structural_Valid_Message (Ctx) @@ -616,11 +674,17 @@ private and Cursors (F).First <= Cursors (F).Last + 1 and Valid_Value (F, Cursors (F).Value))) and then ((if - Structural_Valid (Cursors (F_Data)) + Structural_Valid (Cursors (F_Length)) then (Valid (Cursors (F_Message_Type)) - and then Cursors (F_Data).Predecessor = F_Message_Type))) - and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Data)))) + and then Cursors (F_Length).Predecessor = F_Message_Type)) + and then (if + Structural_Valid (Cursors (F_Data)) + then + (Valid (Cursors (F_Length)) + and then Cursors (F_Data).Predecessor = F_Length))) + and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length))) + and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data)))) and then (if Structural_Valid (Cursors (F_Message_Type)) then @@ -628,11 +692,17 @@ private and then Cursors (F_Message_Type).Predecessor = F_Initial and then Cursors (F_Message_Type).First = First and then (if - Structural_Valid (Cursors (F_Data)) + Structural_Valid (Cursors (F_Length)) then - Cursors (F_Data).Last - Cursors (F_Data).First + 1 = 24 - and then Cursors (F_Data).Predecessor = F_Message_Type - and then Cursors (F_Data).First = Cursors (F_Message_Type).Last + 1))); + Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 8 + and then Cursors (F_Length).Predecessor = F_Message_Type + and then Cursors (F_Length).First = Cursors (F_Message_Type).Last + 1 + and then (if + Structural_Valid (Cursors (F_Data)) + then + Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8 + and then Cursors (F_Data).Predecessor = F_Length + and then Cursors (F_Data).First = Cursors (F_Length).Last + 1)))); pragma Warnings (On, """Buffer"" is not modified, could be of access constant type"); @@ -672,6 +742,8 @@ private ((case Fld is when F_Message_Type => RFLX.Universal.Valid_Option_Type (Val), + when F_Length => + RFLX.Test.Valid_Length (Val), when F_Data => True)); @@ -680,15 +752,15 @@ private function Field_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Fld is - when F_Message_Type | F_Data => + when F_Message_Type | F_Length | F_Data => True)); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is ((case Fld is - when F_Message_Type => + when F_Message_Type | F_Length => 8, when F_Data => - 24)); + RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8)); function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is ((if Fld = F_Message_Type then Ctx.First else Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1)); @@ -709,9 +781,12 @@ private True, when F_Message_Type => Ctx.Cursors (Fld).Predecessor = F_Initial, - when F_Data => + when F_Length => (Valid (Ctx.Cursors (F_Message_Type)) and Ctx.Cursors (Fld).Predecessor = F_Message_Type), + when F_Data => + (Valid (Ctx.Cursors (F_Length)) + and Ctx.Cursors (Fld).Predecessor = F_Length), when F_Final => (Structural_Valid (Ctx.Cursors (F_Data)) and Ctx.Cursors (Fld).Predecessor = F_Data))); @@ -755,6 +830,9 @@ private function Get_Message_Type (Ctx : Context) return RFLX.Universal.Option_Type is (To_Actual (Ctx.Cursors (F_Message_Type).Value)); + function Get_Length (Ctx : Context) return RFLX.Test.Length is + (To_Actual (Ctx.Cursors (F_Length).Value)); + function Valid_Size (Ctx : Context; Fld : Field; Size : RFLX_Types.Bit_Length) return Boolean is (Size = Field_Size (Ctx, Fld)) with @@ -776,4 +854,4 @@ private function Valid_Structure (Struct : Structure) return Boolean is (RFLX.Universal.Valid_Option_Type (Struct.Message_Type)); -end RFLX.Fixed_Size.Simple_Message; +end RFLX.Test.Definite_Message; diff --git a/tests/integration/session_functions/generated/rflx-test-session.adb b/tests/integration/session_functions/generated/rflx-test-session.adb index d3b158fad..8e57fb708 100644 --- a/tests/integration/session_functions/generated/rflx-test-session.adb +++ b/tests/integration/session_functions/generated/rflx-test-session.adb @@ -45,21 +45,30 @@ is is Valid : Test.Result; Message_Type : Universal.Option_Type; + Length : Test.Length; begin pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null and Ctx.P.Slots.Slot_Ptr_2 = null); Get_Message_Type (Ctx, Message_Type); Valid_Message (Ctx, Message_Type, True, Valid); + if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Data) then + Length := Test.Length (Universal.Message.Field_Size (Ctx.P.Message_Ctx, Universal.Message.F_Data) / 8); + else + Ctx.P.Next_State := S_Terminated; + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + goto Finalize_Process; + end if; if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Data) then declare - Fixed_Size_Message : Fixed_Size.Simple_Message.Structure; - RFLX_Create_Message_Arg_1_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0); - RFLX_Create_Message_Arg_1_Message_Length : constant RFLX_Types.Length := RFLX_Types.To_Length (Universal.Message.Field_Size (Ctx.P.Message_Ctx, Universal.Message.F_Data)) + 1; + Definite_Message : Test.Definite_Message.Structure; + RFLX_Create_Message_Arg_2_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0); + RFLX_Create_Message_Arg_2_Message_Length : constant RFLX_Types.Length := RFLX_Types.To_Length (Universal.Message.Field_Size (Ctx.P.Message_Ctx, Universal.Message.F_Data)) + 1; begin - Universal.Message.Get_Data (Ctx.P.Message_Ctx, RFLX_Create_Message_Arg_1_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_1_Message_Length) - 2)); - Create_Message (Ctx, Message_Type, RFLX_Create_Message_Arg_1_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_1_Message_Length) - 2), Fixed_Size_Message); - if Fixed_Size.Simple_Message.Valid_Structure (Fixed_Size_Message) then - Fixed_Size.Simple_Message.To_Context (Fixed_Size_Message, Ctx.P.Fixed_Size_Message_Ctx); + Universal.Message.Get_Data (Ctx.P.Message_Ctx, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length) - 2)); + Create_Message (Ctx, Message_Type, Length, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length) - 2), Definite_Message); + if Test.Definite_Message.Valid_Structure (Definite_Message) then + Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx); else Ctx.P.Next_State := S_Terminated; pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null @@ -92,14 +101,67 @@ is begin pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null and Ctx.P.Slots.Slot_Ptr_2 = null); - Ctx.P.Next_State := S_Terminated; + Ctx.P.Next_State := S_Process_2; pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null and Ctx.P.Slots.Slot_Ptr_2 = null); end Reply; + procedure Process_2 (Ctx : in out Context'Class) with + Pre => + Initialized (Ctx), + Post => + Initialized (Ctx) + is + Length : Test.Length; + begin + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + Length := Test.Length (Universal.Message.Size (Ctx.P.Message_Ctx) / 8); + declare + Definite_Message : Test.Definite_Message.Structure; + RFLX_Create_Message_Arg_2_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0); + RFLX_Create_Message_Arg_2_Message_Length : constant RFLX_Types.Length := Universal.Message.Byte_Size (Ctx.P.Message_Ctx); + begin + if not Universal.Message.Structural_Valid_Message (Ctx.P.Message_Ctx) then + Ctx.P.Next_State := S_Terminated; + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + goto Finalize_Process_2; + end if; + Universal.Message.Message_Data (Ctx.P.Message_Ctx, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length + 1) - 2)); + Create_Message (Ctx, (Known => True, Enum => Universal.OT_Data), Length, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length + 1) - 2), Definite_Message); + if Test.Definite_Message.Valid_Structure (Definite_Message) then + Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx); + else + Ctx.P.Next_State := S_Terminated; + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + goto Finalize_Process_2; + end if; + end; + Ctx.P.Next_State := S_Reply_2; + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + <> + end Process_2; + + procedure Reply_2 (Ctx : in out Context'Class) with + Pre => + Initialized (Ctx), + Post => + Initialized (Ctx) + is + begin + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + Ctx.P.Next_State := S_Terminated; + pragma Assert (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 = null); + end Reply_2; + procedure Initialize (Ctx : in out Context'Class) is Message_Buffer : RFLX_Types.Bytes_Ptr; - Fixed_Size_Message_Buffer : RFLX_Types.Bytes_Ptr; + Definite_Message_Buffer : RFLX_Types.Bytes_Ptr; begin Test.Session_Allocator.Initialize (Ctx.P.Slots, Ctx.P.Memory); Message_Buffer := Ctx.P.Slots.Slot_Ptr_1; @@ -107,26 +169,26 @@ is Ctx.P.Slots.Slot_Ptr_1 := null; pragma Warnings (On, "unused assignment"); Universal.Message.Initialize (Ctx.P.Message_Ctx, Message_Buffer); - Fixed_Size_Message_Buffer := Ctx.P.Slots.Slot_Ptr_2; + Definite_Message_Buffer := Ctx.P.Slots.Slot_Ptr_2; pragma Warnings (Off, "unused assignment"); Ctx.P.Slots.Slot_Ptr_2 := null; pragma Warnings (On, "unused assignment"); - Fixed_Size.Simple_Message.Initialize (Ctx.P.Fixed_Size_Message_Ctx, Fixed_Size_Message_Buffer); + Test.Definite_Message.Initialize (Ctx.P.Definite_Message_Ctx, Definite_Message_Buffer); Ctx.P.Next_State := S_Start; end Initialize; procedure Finalize (Ctx : in out Context'Class) is Message_Buffer : RFLX_Types.Bytes_Ptr; - Fixed_Size_Message_Buffer : RFLX_Types.Bytes_Ptr; + Definite_Message_Buffer : RFLX_Types.Bytes_Ptr; begin pragma Warnings (Off, """Ctx.P.Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); Universal.Message.Take_Buffer (Ctx.P.Message_Ctx, Message_Buffer); pragma Warnings (On, """Ctx.P.Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); Ctx.P.Slots.Slot_Ptr_1 := Message_Buffer; - pragma Warnings (Off, """Ctx.P.Fixed_Size_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); - Fixed_Size.Simple_Message.Take_Buffer (Ctx.P.Fixed_Size_Message_Ctx, Fixed_Size_Message_Buffer); - pragma Warnings (On, """Ctx.P.Fixed_Size_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); - Ctx.P.Slots.Slot_Ptr_2 := Fixed_Size_Message_Buffer; + pragma Warnings (Off, """Ctx.P.Definite_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + Test.Definite_Message.Take_Buffer (Ctx.P.Definite_Message_Ctx, Definite_Message_Buffer); + pragma Warnings (On, """Ctx.P.Definite_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + Ctx.P.Slots.Slot_Ptr_2 := Definite_Message_Buffer; Test.Session_Allocator.Finalize (Ctx.P.Slots); Ctx.P.Next_State := S_Terminated; end Finalize; @@ -141,7 +203,7 @@ is case Ctx.P.Next_State is when S_Start => Universal.Message.Reset (Ctx.P.Message_Ctx, Ctx.P.Message_Ctx.First, Ctx.P.Message_Ctx.First - 1); - when S_Process | S_Reply | S_Terminated => + when S_Process | S_Reply | S_Process_2 | S_Reply_2 | S_Terminated => null; end case; end Reset_Messages_Before_Write; @@ -155,6 +217,10 @@ is Process (Ctx); when S_Reply => Reply (Ctx); + when S_Process_2 => + Process_2 (Ctx); + when S_Reply_2 => + Reply_2 (Ctx); when S_Terminated => null; end case; @@ -162,7 +228,7 @@ is end Tick; function In_IO_State (Ctx : Context'Class) return Boolean is - (Ctx.P.Next_State in S_Start | S_Reply); + (Ctx.P.Next_State in S_Start | S_Reply | S_Reply_2); procedure Run (Ctx : in out Context'Class) is begin @@ -189,14 +255,14 @@ is begin Buffer (Buffer'First .. RFLX_Types.Index (Buffer_Last)) := Message_Buffer (RFLX_Types.Index (RFLX_Types.Length (Message_Buffer'First) + Offset) .. Message_Buffer'First - 2 + RFLX_Types.Index (Offset + 1) + Length); end Read; - procedure Fixed_Size_Simple_Message_Read is new Fixed_Size.Simple_Message.Generic_Read (Read, Read_Pre); + procedure Test_Definite_Message_Read is new Test.Definite_Message.Generic_Read (Read, Read_Pre); begin Buffer := (others => 0); case Chan is when C_Channel => case Ctx.P.Next_State is - when S_Reply => - Fixed_Size_Simple_Message_Read (Ctx.P.Fixed_Size_Message_Ctx); + when S_Reply | S_Reply_2 => + Test_Definite_Message_Read (Ctx.P.Definite_Message_Ctx); when others => null; end case; diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads index 10cf79b5d..226047e0d 100644 --- a/tests/integration/session_functions/generated/rflx-test-session.ads +++ b/tests/integration/session_functions/generated/rflx-test-session.ads @@ -5,8 +5,7 @@ with RFLX.Test.Session_Allocator; with RFLX.RFLX_Types; with RFLX.Universal; with RFLX.Universal.Message; -with RFLX.Fixed_Size; -with RFLX.Fixed_Size.Simple_Message; +with RFLX.Test.Definite_Message; package RFLX.Test.Session with SPARK_Mode @@ -18,7 +17,7 @@ is type Channel is (C_Channel); - type State is (S_Start, S_Process, S_Reply, S_Terminated); + type State is (S_Start, S_Process, S_Reply, S_Process_2, S_Reply_2, S_Terminated); type Private_Context is private; @@ -34,7 +33,7 @@ is Post'Class => Initialized (Ctx); - procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Data : RFLX_Types.Bytes; RFLX_Result : out RFLX.Fixed_Size.Simple_Message.Structure) is abstract with + procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Length : RFLX.Test.Length; Data : RFLX_Types.Bytes; RFLX_Result : out RFLX.Test.Definite_Message.Structure) is abstract with Pre'Class => Initialized (Ctx), Post'Class => @@ -129,23 +128,23 @@ private record Next_State : State := S_Start; Message_Ctx : Universal.Message.Context; - Fixed_Size_Message_Ctx : Fixed_Size.Simple_Message.Context; + Definite_Message_Ctx : Test.Definite_Message.Context; Slots : Test.Session_Allocator.Slots; Memory : Test.Session_Allocator.Memory; end record; function Uninitialized (Ctx : Context'Class) return Boolean is (not Universal.Message.Has_Buffer (Ctx.P.Message_Ctx) - and not Fixed_Size.Simple_Message.Has_Buffer (Ctx.P.Fixed_Size_Message_Ctx) + and not Test.Definite_Message.Has_Buffer (Ctx.P.Definite_Message_Ctx) and Test.Session_Allocator.Uninitialized (Ctx.P.Slots)); function Global_Initialized (Ctx : Context'Class) return Boolean is (Universal.Message.Has_Buffer (Ctx.P.Message_Ctx) and then Ctx.P.Message_Ctx.Buffer_First = RFLX_Types.Index'First and then Ctx.P.Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095 - and then Fixed_Size.Simple_Message.Has_Buffer (Ctx.P.Fixed_Size_Message_Ctx) - and then Ctx.P.Fixed_Size_Message_Ctx.Buffer_First = RFLX_Types.Index'First - and then Ctx.P.Fixed_Size_Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095); + and then Test.Definite_Message.Has_Buffer (Ctx.P.Definite_Message_Ctx) + and then Ctx.P.Definite_Message_Ctx.Buffer_First = RFLX_Types.Index'First + and then Ctx.P.Definite_Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095); function Initialized (Ctx : Context'Class) return Boolean is (Global_Initialized (Ctx) @@ -161,9 +160,9 @@ private ((case Chan is when C_Channel => (case Ctx.P.Next_State is - when S_Reply => - Fixed_Size.Simple_Message.Structural_Valid_Message (Ctx.P.Fixed_Size_Message_Ctx) - and Fixed_Size.Simple_Message.Byte_Size (Ctx.P.Fixed_Size_Message_Ctx) > 0, + when S_Reply | S_Reply_2 => + Test.Definite_Message.Structural_Valid_Message (Ctx.P.Definite_Message_Ctx) + and Test.Definite_Message.Byte_Size (Ctx.P.Definite_Message_Ctx) > 0, when others => False))); @@ -171,8 +170,8 @@ private ((case Chan is when C_Channel => (case Ctx.P.Next_State is - when S_Reply => - Fixed_Size.Simple_Message.Byte_Size (Ctx.P.Fixed_Size_Message_Ctx), + when S_Reply | S_Reply_2 => + Test.Definite_Message.Byte_Size (Ctx.P.Definite_Message_Ctx), when others => RFLX_Types.Unreachable))); diff --git a/tests/integration/session_functions/generated/rflx-test.ads b/tests/integration/session_functions/generated/rflx-test.ads index 6f2490890..e768bbfe6 100644 --- a/tests/integration/session_functions/generated/rflx-test.ads +++ b/tests/integration/session_functions/generated/rflx-test.ads @@ -39,4 +39,20 @@ is pragma Warnings (On, "unreachable branch"); + type Length is range 0 .. 2**8 - 1 with + Size => + 8; + + function Valid_Length (Val : RFLX.RFLX_Types.U64) return Boolean is + (Val <= 255); + + function To_U64 (Val : RFLX.Test.Length) return RFLX.RFLX_Types.U64 is + (RFLX.RFLX_Types.U64 (Val)); + + function To_Actual (Val : RFLX.RFLX_Types.U64) return RFLX.Test.Length is + (RFLX.Test.Length (Val)) + with + Pre => + Valid_Length (Val); + end RFLX.Test; diff --git a/tests/integration/session_functions/src/session.adb b/tests/integration/session_functions/src/session.adb index a45a1d524..6061869b4 100644 --- a/tests/integration/session_functions/src/session.adb +++ b/tests/integration/session_functions/src/session.adb @@ -15,16 +15,16 @@ is procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; + Length : RFLX.Test.Length; Data : RFLX.RFLX_Types.Bytes; - Result : out RFLX.Fixed_Size.Simple_Message.Structure) + Result : out RFLX.Test.Definite_Message.Structure) is + use type RFLX.RFLX_Types.Index; begin Result.Message_Type := Message_Type; - if Result.Data'Length = Data'Length then - Result.Data := Data; - else - Result.Data := (others => 0); - end if; + Result.Length := Length; + Result.Data := (others => 0); + Result.Data (Result.Data'First .. Result.Data'First + Data'Length - 1) := Data; end Create_Message; overriding diff --git a/tests/integration/session_functions/src/session.ads b/tests/integration/session_functions/src/session.ads index 727825b01..5aae5c87b 100644 --- a/tests/integration/session_functions/src/session.ads +++ b/tests/integration/session_functions/src/session.ads @@ -2,7 +2,7 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); with RFLX.RFLX_Types; with RFLX.Universal; -with RFLX.Fixed_Size.Simple_Message; +with RFLX.Test.Definite_Message; with RFLX.Test.Session; package Session with @@ -24,8 +24,9 @@ is procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; + Length : RFLX.Test.Length; Data : RFLX.RFLX_Types.Bytes; - Result : out RFLX.Fixed_Size.Simple_Message.Structure); + Result : out RFLX.Test.Definite_Message.Structure); overriding procedure Valid_Message diff --git a/tests/integration/session_functions/test.rflx b/tests/integration/session_functions/test.rflx index bcbed139b..b1beb3b7d 100644 --- a/tests/integration/session_functions/test.rflx +++ b/tests/integration/session_functions/test.rflx @@ -1,10 +1,19 @@ -with Fixed_Size; with Universal; package Test is type Result is (M_Valid, M_Invalid) with Size => 2; + type Length is range 0 .. 2 ** 8 - 1 with Size => 8; + + type Definite_Message is + message + Message_Type : Universal::Option_Type; + Length : Length; + Data : Opaque + with Size => Length * 8; + end message; + generic Channel : Channel with Readable, Writable; -- §S-P-C-RW -- §S-P-F-R-S @@ -12,8 +21,9 @@ package Test is -- §S-P-F-P-S, §S-P-F-P-O, §S-P-F-R-M with function Create_Message (Message_Type : Universal::Option_Type; + Length : Length; Data : Opaque) - return Fixed_Size::Simple_Message; + return Definite_Message; -- §S-P-F-P-S, §S-P-F-R-S with function Valid_Message (Message_Type : Universal::Option_Type; @@ -24,7 +34,7 @@ package Test is Final => Terminated is Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - Fixed_Size_Message : Fixed_Size::Simple_Message; -- §S-D-V-T-M, §S-D-V-E-N + Definite_Message : Definite_Message; -- §S-D-V-T-M, §S-D-V-E-N begin state Start is begin @@ -40,10 +50,13 @@ package Test is state Process is Valid : Result; -- §S-S-D-V-T-SC Message_Type : Universal::Option_Type; -- §S-S-D-V-T-SC, §S-S-D-V-E-N + Length : Length; begin Message_Type := Get_Message_Type; -- §S-S-A-A-CL, §S-E-CL-N - Valid := Valid_Message (Message_Type, True); -- §S-S-A-A-CL, §S-E-CL-L - Fixed_Size_Message := Create_Message (Message_Type, Message.Data); -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S + Valid := Valid_Message (Message_Type, True); -- §S-S-A-A-CL, §S-E-CL-L + Length := Message.Data'Size / 8; -- §S-S-A-A-ME + -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S + Definite_Message := Create_Message (Message_Type, Length, Message.Data); transition goto Reply if Valid = M_Valid -- §S-S-T-BE @@ -54,11 +67,30 @@ package Test is state Reply is begin - Channel'Write (Fixed_Size_Message); -- §S-S-A-WR-V + Channel'Write (Definite_Message); -- §S-S-A-WR-V transition - goto Terminated -- §S-S-T-N + goto Process_2 -- §S-S-T-N end Reply; + state Process_2 is + Length : Length; + begin + Length := Message'Size / 8; -- §S-S-A-A-ME + -- §S-S-A-A-CL, §S-E-CL-L, §S-E-CL-V, §S-E-CL-OAT + Definite_Message := Create_Message (Universal::OT_Data, Length, Message'Opaque); + transition + goto Reply_2 -- §S-S-T-N + exception + goto Terminated -- §S-S-E + end Process_2; + + state Reply_2 is + begin + Channel'Write (Definite_Message); -- §S-S-A-WR-V + transition + goto Terminated -- §S-S-T-N + end Reply_2; + state Terminated is null state; -- §S-S-N end Session; diff --git a/tests/unit/integration_test.py b/tests/unit/integration_test.py index b05a6a11e..718d09464 100644 --- a/tests/unit/integration_test.py +++ b/tests/unit/integration_test.py @@ -129,6 +129,7 @@ def test_rfi_get_size() -> None: # pylint: disable = protected-access integration._add_integration_object(Path("p.rfi"), session_object, error) error.propagate() + assert integration.get_size(ID("P::S"), None, None) == 1024 assert integration.get_size(ID("P::S"), ID("x"), ID("S")) == 1024 assert integration.get_size(ID("P::S"), ID("x"), ID("S")) == 1024 assert integration.get_size(ID("P::S"), ID("x"), None) == 1024