diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ffcf3f3a..4cd6828f8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,7 +21,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - LLVM exception in addition to Apache-2.0 for generated code (eng/recordflux/RecordFlux#1671) - Improve suggestions when a package name is not correct (eng/recordflux/RecordFlux#1611) - Severities of error messages (eng/recordflux/RecordFlux#1698, eng/recordflux/RecordFlux#1685) -- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707) +- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707, eng/recordflux/RecordFlux#1706) - Cache directory from `$HOME/.cache/RecordFlux` to `$PWD/.rflx_cache` (eng/recordflux/RecordFlux#1723) ### Fixed diff --git a/rflx/generator/message.py b/rflx/generator/message.py index a8d66252b..955f48a99 100644 --- a/rflx/generator/message.py +++ b/rflx/generator/message.py @@ -22,7 +22,6 @@ Component, Constrained, ContractCases, - Decreases, DefaultInitialCondition, Depends, Discriminant, @@ -79,7 +78,6 @@ Sub, SubprogramBody, SubprogramDeclaration, - SubprogramVariant, UnitPart, UseTypeClause, ValueRange, @@ -636,7 +634,7 @@ def create_field_size_internal_function(message: Message, prefix: str) -> UnitPa def create_field_first_internal_function(message: Message, prefix: str) -> UnitPart: def recursive_call(fld: Field) -> expr.Expr: return expr.Call( - "Field_First_Internal", + "Field_First_" + fld.name, rty.BIT_INDEX, [ expr.Variable("Cursors"), @@ -645,7 +643,6 @@ def recursive_call(fld: Field) -> expr.Expr: expr.Variable("Written_Last"), expr.Variable("Buffer"), *[expr.Variable(param.name) for param in message.parameter_types], - expr.Variable(fld.affixed_name), ], ) @@ -715,6 +712,63 @@ def fld_first_expr(fld: Field) -> expr.Expr: dist.substituted(field_size_substitution), ).simplified() + param_args = [Variable(param.name) for param in message.parameter_types] + + def precond(fld: str) -> Precondition: + return Precondition( + AndThen( + Call( + "Cursors_Invariant", + [ + Variable("Cursors"), + Variable("First"), + Variable("Verified_Last"), + ], + ), + Call( + "Valid_Predecessors_Invariant", + [ + Variable("Cursors"), + Variable("First"), + Variable("Verified_Last"), + Variable("Written_Last"), + Variable("Buffer"), + *param_args, + ], + ), + Call( + "Valid_Next_Internal", + [ + Variable("Cursors"), + Variable("First"), + Variable("Verified_Last"), + Variable("Written_Last"), + Variable("Buffer"), + *param_args, + Variable(fld), + ], + ), + ), + ) + + def fld_first_func(fld: Field) -> ExpressionFunctionDeclaration: + return ExpressionFunctionDeclaration( + FunctionSpecification( + "Field_First_" + fld.name, + "RFLX_Types.Bit_Index'Base", + [ + Parameter(["Cursors"], "Field_Cursors"), + Parameter(["First"], const.TYPES_BIT_INDEX), + Parameter(["Verified_Last"], const.TYPES_BIT_LENGTH), + Parameter(["Written_Last"], const.TYPES_BIT_LENGTH), + Parameter(["Buffer"], const.TYPES_BYTES_PTR), + *common.message_parameters(message), + ], + ), + expr_conv.to_ada(fld_first_expr(fld)), + [precond(fld.affixed_name)], + ) + specification = FunctionSpecification( "Field_First_Internal", "RFLX_Types.Bit_Index'Base", @@ -729,59 +783,23 @@ def fld_first_expr(fld: Field) -> expr.Expr: ], ) - param_args = [Variable(param.name) for param in message.parameter_types] - return UnitPart( [], private=common.wrap_warning( [ + *[fld_first_func(fld) for fld in message.fields], ExpressionFunctionDeclaration( specification, Case( Variable("Fld"), [ - (Variable(f.affixed_name), expr_conv.to_ada(fld_first_expr(f))) + (Variable(f.affixed_name), expr_conv.to_ada(recursive_call(f))) for f in message.fields ], ), [ - Precondition( - AndThen( - Call( - "Cursors_Invariant", - [ - Variable("Cursors"), - Variable("First"), - Variable("Verified_Last"), - ], - ), - Call( - "Valid_Predecessors_Invariant", - [ - Variable("Cursors"), - Variable("First"), - Variable("Verified_Last"), - Variable("Written_Last"), - Variable("Buffer"), - *param_args, - ], - ), - Call( - "Valid_Next_Internal", - [ - Variable("Cursors"), - Variable("First"), - Variable("Verified_Last"), - Variable("Written_Last"), - Variable("Buffer"), - *param_args, - Variable("Fld"), - ], - ), - ), - ), + precond("Fld"), Postcondition(TRUE), - SubprogramVariant(Decreases(Variable("Fld"))), ], ), ], diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads index 30230540d..30892d7aa 100644 --- a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads +++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads @@ -590,22 +590,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A); + + function Field_First_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 1) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_A => - First, + Field_First_A (Cursors, First, Verified_Last, Written_Last, Buffer), when F_B => - First + 1)) + Field_First_B (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads b/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads index 58189cb51..97c86073f 100644 --- a/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads +++ b/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads @@ -702,24 +702,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Tag => - First, + Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Value => - First + 24)) + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads index 9e7ee98dc..d0888f1e0 100644 --- a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads +++ b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads @@ -560,32 +560,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_F1 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F1); + + function Field_First_F2 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is + ((if + Well_Formed (Cursors (F_F1)) + and then True + then + First + 8 + elsif + True + then + First + 0 + else + RFLX_Types.Unreachable)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F2); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_F1 => - First, + Field_First_F1 (Cursors, First, Verified_Last, Written_Last, Buffer, P), when F_F2 => - (if - Well_Formed (Cursors (F_F1)) - and then True - then - First + 8 - elsif - True - then - First + 0 - else - RFLX_Types.Unreachable))) + Field_First_F2 (Cursors, First, Verified_Last, Written_Last, Buffer, P))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads index 1422502b6..2dbd428b6 100644 --- a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads +++ b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads @@ -611,20 +611,25 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Data => - First)) + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads index 290b4fe6b..eae3e29d3 100644 --- a/tests/feature/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/feature/parameterized_messages/generated/rflx-test-message.ads @@ -710,22 +710,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data); + + function Field_First_Extension (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is + (Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Data => - First, + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended), when F_Extension => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data))) + Field_First_Extension (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads b/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads index 80bfc50a9..757999fff 100644 --- a/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads +++ b/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads @@ -548,20 +548,25 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Value => - First)) + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg.ads b/tests/feature/session_endianness/generated/rflx-messages-msg.ads index ccf29f6d5..0b2cad585 100644 --- a/tests/feature/session_endianness/generated/rflx-messages-msg.ads +++ b/tests/feature/session_endianness/generated/rflx-messages-msg.ads @@ -586,22 +586,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A); + + function Field_First_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_A => - First, + Field_First_A (Cursors, First, Verified_Last, Written_Last, Buffer), when F_B => - First + 32)) + Field_First_B (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads b/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads index 7b31ee5d2..d69ef10f9 100644 --- a/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads +++ b/tests/feature/session_endianness/generated/rflx-messages-msg_le.ads @@ -586,22 +586,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_C (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C); + + function Field_First_D (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_C => - First, + Field_First_C (Cursors, First, Verified_Last, Written_Last, Buffer), when F_D => - First + 32)) + Field_First_D (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads index abda2059e..a2625039b 100644 --- a/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads +++ b/tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads @@ -626,24 +626,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_X_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A); + + function Field_First_X_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B); + + function Field_First_Y (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 64) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_X_A => - First, + Field_First_X_A (Cursors, First, Verified_Last, Written_Last, Buffer), when F_X_B => - First + 32, + Field_First_X_B (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Y => - First + 64)) + Field_First_Y (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_functions/generated/rflx-test-definite_message.ads b/tests/feature/session_functions/generated/rflx-test-definite_message.ads index 209903ebd..ff05e960f 100644 --- a/tests/feature/session_functions/generated/rflx-test-definite_message.ads +++ b/tests/feature/session_functions/generated/rflx-test-definite_message.ads @@ -735,24 +735,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Message_Type => - First, + Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Data => - First + 16)) + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads b/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads index cfc8cb9aa..902ef6213 100644 --- a/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads +++ b/tests/feature/session_message_optimization/generated/rflx-test-option_data.ads @@ -677,22 +677,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Length => - First, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Data => - First + 16)) + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads index 58189cb51..97c86073f 100644 --- a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads +++ b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads @@ -702,24 +702,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Tag => - First, + Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Value => - First + 24)) + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/shared/generated/rflx-universal-message.ads b/tests/feature/shared/generated/rflx-universal-message.ads index 3a3141e29..f46d930d1 100644 --- a/tests/feature/shared/generated/rflx-universal-message.ads +++ b/tests/feature/shared/generated/rflx-universal-message.ads @@ -1305,52 +1305,107 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + ((if + Well_Formed (Cursors (F_Length)) + and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Data)) + then + First + 24 + elsif + Well_Formed (Cursors (F_Message_Type)) + and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data)) + then + First + 8 + else + RFLX_Types.Unreachable)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + + function Field_First_Option_Types (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Types); + + function Field_First_Options (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + ((if + Well_Formed (Cursors (F_Length)) + and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Options)) + then + First + 24 + elsif + Well_Formed (Cursors (F_Message_Type)) + and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options)) + then + First + 8 + else + RFLX_Types.Unreachable)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options); + + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + + function Field_First_Values (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Values); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Message_Type => - First, + Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Data => - (if - Well_Formed (Cursors (F_Length)) - and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Data)) - then - First + 24 - elsif - Well_Formed (Cursors (F_Message_Type)) - and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data)) - then - First + 8 - else - RFLX_Types.Unreachable), + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Option_Types => - First + 24, + Field_First_Option_Types (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Options => - (if - Well_Formed (Cursors (F_Length)) - and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Options)) - then - First + 24 - elsif - Well_Formed (Cursors (F_Message_Type)) - and then RFLX_Types.Base_Integer (Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options)) - then - First + 8 - else - RFLX_Types.Unreachable), - when F_Value | F_Values => - First + 24)) + Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Value => + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Values => + Field_First_Values (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/feature/shared/generated/rflx-universal-option.ads b/tests/feature/shared/generated/rflx-universal-option.ads index 4f18e2962..0201955d4 100644 --- a/tests/feature/shared/generated/rflx-universal-option.ads +++ b/tests/feature/shared/generated/rflx-universal-option.ads @@ -702,24 +702,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Option_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Type); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Option_Type => - First, + Field_First_Option_Type (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Data => - First + 24)) + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index eb8436da9..7ab82340e 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -704,24 +704,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Tag => - First, + Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Value => - First + 24)) + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads index bf0babdcd..389effc2d 100644 --- a/tests/spark/generated/rflx-enumeration-message.ads +++ b/tests/spark/generated/rflx-enumeration-message.ads @@ -548,20 +548,25 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Priority (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Priority); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Priority => - First)) + Field_First_Priority (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index 45789a6c3..bc534a9fd 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -865,41 +865,96 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Destination (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination); + + function Field_First_Source (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 48) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source); + + function Field_First_Type_Length_TPID (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 96) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length_TPID); + + function Field_First_TPID (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 96) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TPID); + + function Field_First_TCI (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 112) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TCI); + + function Field_First_Type_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + ((if + Well_Formed (Cursors (F_TCI)) + and then True + then + First + 128 + elsif + Well_Formed (Cursors (F_Type_Length_TPID)) + and then Cursors (F_Type_Length_TPID).Value /= 16#8100# + then + First + 96 + else + RFLX_Types.Unreachable)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length); + + function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Type_Length (Cursors, First, Verified_Last, Written_Last, Buffer) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Destination => - First, + Field_First_Destination (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Source => - First + 48, - when F_Type_Length_TPID | F_TPID => - First + 96, + Field_First_Source (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Type_Length_TPID => + Field_First_Type_Length_TPID (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_TPID => + Field_First_TPID (Cursors, First, Verified_Last, Written_Last, Buffer), when F_TCI => - First + 112, + Field_First_TCI (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Type_Length => - (if - Well_Formed (Cursors (F_TCI)) - and then True - then - First + 128 - elsif - Well_Formed (Cursors (F_Type_Length_TPID)) - and then Cursors (F_Type_Length_TPID).Value /= 16#8100# - then - First + 96 - else - RFLX_Types.Unreachable), + Field_First_Type_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Payload => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Type_Length) + 16)) + Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index 6117d0d9a..c2c21d50e 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.ads @@ -620,20 +620,25 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Payload => - First)) + Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 898cafb60..d0aa78c33 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -680,22 +680,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Message_Type (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Message_Type => - First, + Field_First_Message_Type (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Data => - First + 8)) + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index 09e585b1b..a6eafeaa4 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -1434,36 +1434,175 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag); + + function Field_First_Code_Destination_Unreachable (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Destination_Unreachable); + + function Field_First_Code_Redirect (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Redirect); + + function Field_First_Code_Time_Exceeded (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Time_Exceeded); + + function Field_First_Code_Zero (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Code_Zero); + + function Field_First_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum); + + function Field_First_Gateway_Internet_Address (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Gateway_Internet_Address); + + function Field_First_Identifier (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Identifier); + + function Field_First_Pointer (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Pointer); + + function Field_First_Unused_32 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Unused_32); + + function Field_First_Sequence_Number (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Sequence_Number); + + function Field_First_Unused_24 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Unused_24); + + function Field_First_Originate_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 48) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Originate_Timestamp); + + function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 48) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data); + + function Field_First_Receive_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 80) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Receive_Timestamp); + + function Field_First_Transmit_Timestamp (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer) + 112) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Transmit_Timestamp); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Tag => - First, - when F_Code_Destination_Unreachable | F_Code_Redirect | F_Code_Time_Exceeded | F_Code_Zero => - First + 8, + Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Code_Destination_Unreachable => + Field_First_Code_Destination_Unreachable (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Code_Redirect => + Field_First_Code_Redirect (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Code_Time_Exceeded => + Field_First_Code_Time_Exceeded (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Code_Zero => + Field_First_Code_Zero (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Checksum => - First + 16, - when F_Gateway_Internet_Address | F_Identifier | F_Pointer | F_Unused_32 => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 16, + Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Gateway_Internet_Address => + Field_First_Gateway_Internet_Address (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Identifier => + Field_First_Identifier (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Pointer => + Field_First_Pointer (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Unused_32 => + Field_First_Unused_32 (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Sequence_Number => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 32, + Field_First_Sequence_Number (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Unused_24 => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 24, - when F_Originate_Timestamp | F_Data => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 48, + Field_First_Unused_24 (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Originate_Timestamp => + Field_First_Originate_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer), + when F_Data => + Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Receive_Timestamp => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 80, + Field_First_Receive_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Transmit_Timestamp => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum) + 112)) + Field_First_Transmit_Timestamp (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index f5167248e..8d2be6a49 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -827,28 +827,65 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Copied (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Copied); + + function Field_First_Option_Class (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 1) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Class); + + function Field_First_Option_Number (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 3) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Number); + + function Field_First_Option_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Length); + + function Field_First_Option_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Option_Data); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Copied => - First, + Field_First_Copied (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Option_Class => - First + 1, + Field_First_Option_Class (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Option_Number => - First + 3, + Field_First_Option_Number (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Option_Length => - First + 8, + Field_First_Option_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Option_Data => - First + 16)) + Field_First_Option_Data (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index b132054cd..ffcd4445a 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -1590,52 +1590,185 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Version (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Version); + + function Field_First_IHL (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 4) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_IHL); + + function Field_First_DSCP (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_DSCP); + + function Field_First_ECN (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 14) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_ECN); + + function Field_First_Total_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Total_Length); + + function Field_First_Identification (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Identification); + + function Field_First_Flag_R (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 48) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_R); + + function Field_First_Flag_DF (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 49) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_DF); + + function Field_First_Flag_MF (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 50) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Flag_MF); + + function Field_First_Fragment_Offset (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 51) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Fragment_Offset); + + function Field_First_TTL (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 64) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_TTL); + + function Field_First_Protocol (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 72) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Protocol); + + function Field_First_Header_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 80) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Header_Checksum); + + function Field_First_Source (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 96) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source); + + function Field_First_Destination (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 128) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination); + + function Field_First_Options (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 160) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options); + + function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Version => - First, + Field_First_Version (Cursors, First, Verified_Last, Written_Last, Buffer), when F_IHL => - First + 4, + Field_First_IHL (Cursors, First, Verified_Last, Written_Last, Buffer), when F_DSCP => - First + 8, + Field_First_DSCP (Cursors, First, Verified_Last, Written_Last, Buffer), when F_ECN => - First + 14, + Field_First_ECN (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Total_Length => - First + 16, + Field_First_Total_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Identification => - First + 32, + Field_First_Identification (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Flag_R => - First + 48, + Field_First_Flag_R (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Flag_DF => - First + 49, + Field_First_Flag_DF (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Flag_MF => - First + 50, + Field_First_Flag_MF (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Fragment_Offset => - First + 51, + Field_First_Fragment_Offset (Cursors, First, Verified_Last, Written_Last, Buffer), when F_TTL => - First + 64, + Field_First_TTL (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Protocol => - First + 72, + Field_First_Protocol (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Header_Checksum => - First + 80, + Field_First_Header_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Source => - First + 96, + Field_First_Source (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Destination => - First + 128, + Field_First_Destination (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Options => - First + 160, + Field_First_Options (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Payload => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Options))) + Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index ece5dff53..ef5bc56ff 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -690,22 +690,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Length => - First, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Payload => - First + 8)) + Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index 2e7a2738e..ee2833028 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -931,26 +931,55 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Integer_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector); + + function Field_First_Enumeration_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Enumeration_Vector); + + function Field_First_AV_Enumeration_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_AV_Enumeration_Vector); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Length => - First, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Integer_Vector => - First + 8, + Field_First_Integer_Vector (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Enumeration_Vector => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector), + Field_First_Enumeration_Vector (Cursors, First, Verified_Last, Written_Last, Buffer), when F_AV_Enumeration_Vector => - Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Integer_Vector) + 16)) + Field_First_AV_Enumeration_Vector (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index 6372c2217..60ca18002 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -675,22 +675,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Messages (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Messages); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Length => - First, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Messages => - First + 8)) + Field_First_Messages (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads index ce49bff7d..8af34c507 100644 --- a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads +++ b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads @@ -677,22 +677,35 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Header (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Header); + + function Field_First_Vector (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Vector); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Header => - First, + Field_First_Header (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Vector => - First + 8)) + Field_First_Vector (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index 58189cb51..97c86073f 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/generated/rflx-tlv-message.ads @@ -702,24 +702,45 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 8) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 24) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Tag => - First, + Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 8, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Value => - First + 24)) + Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result"); diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index 5204da7ce..b190a22d4 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -825,28 +825,65 @@ private pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + function Field_First_Source_Port (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Source_Port); + + function Field_First_Destination_Port (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 16) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Destination_Port); + + function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 32) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length); + + function Field_First_Checksum (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 48) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Checksum); + + function Field_First_Payload (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is + (First + 64) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Payload); + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is ((case Fld is when F_Source_Port => - First, + Field_First_Source_Port (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Destination_Port => - First + 16, + Field_First_Destination_Port (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Length => - First + 32, + Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Checksum => - First + 48, + Field_First_Checksum (Cursors, First, Verified_Last, Written_Last, Buffer), when F_Payload => - First + 64)) + Field_First_Payload (Cursors, First, Verified_Last, Written_Last, Buffer))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), Post => - True, - Subprogram_Variant => - (Decreases => - Fld); + True; pragma Warnings (On, "postcondition does not mention function result");