From ee47a40c074251c61800d767b7b08e8e47007176 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Fri, 3 Nov 2023 10:47:51 +0900 Subject: [PATCH] Remove unused code - Remove assignment of invalid field - Remove Successor function, was only used in said assignment For eng/RecordFlux/RecordFlux#1448 --- CHANGELOG.md | 1 + rflx/generator/common.py | 13 --- rflx/generator/generator.py | 6 - rflx/generator/message.py | 70 ------------ .../generated/rflx-test-message.adb | 15 --- .../generated/rflx-test-message.adb | 27 ----- .../generated/rflx-test-definite_message.adb | 19 ---- .../generated/rflx-test-option_data.adb | 17 --- .../generated/rflx-tlv-message.adb | 28 ----- .../generated/rflx-universal-message.adb | 66 ----------- .../generated/rflx-universal-option.adb | 28 ----- .../generated/rflx-derivation-message.adb | 28 ----- tests/spark/generated/rflx-ethernet-frame.adb | 51 --------- .../generated/rflx-expression-message.adb | 20 ---- .../rflx-fixed_size-simple_message.adb | 22 ---- tests/spark/generated/rflx-icmp-message.adb | 103 ------------------ tests/spark/generated/rflx-ipv4-option.adb | 49 --------- tests/spark/generated/rflx-ipv4-packet.adb | 59 ---------- .../generated/rflx-sequence-inner_message.adb | 17 --- .../spark/generated/rflx-sequence-message.adb | 26 ----- .../rflx-sequence-messages_message.adb | 18 --- ...-sequence_size_defined_by_message_size.adb | 18 --- tests/spark/generated/rflx-tlv-message.adb | 28 ----- tests/spark/generated/rflx-udp-datagram.adb | 23 ---- 24 files changed, 1 insertion(+), 751 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 640644c9d..67f909e2c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changed - Syntax for passing repeated `-i` and `-v` options to `rflx validate` (eng/recordflux/RecordFlux#1441) +- Simplified setter code and removed internal `Successor` function (eng/recordflux/RecordFlux#1448) ### Fixed diff --git a/rflx/generator/common.py b/rflx/generator/common.py index 7091bccd3..552ecb860 100644 --- a/rflx/generator/common.py +++ b/rflx/generator/common.py @@ -708,19 +708,6 @@ def initialize_field_statements( ("Value", Number(0)), ), ), - Assignment( - Indexed( - Variable("Ctx.Cursors"), - Call( - "Successor", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - ), - NamedAggregate( - ("State", Variable("S_Invalid")), - ("others", Variable("<>")), - ), - ), ] diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py index 55fdd290c..35af1286c 100644 --- a/rflx/generator/generator.py +++ b/rflx/generator/generator.py @@ -577,12 +577,6 @@ def _create_message(self, message: Message) -> dict[ID, Unit]: # noqa: PLR0912 scalar_fields, composite_fields, ), - self._executor.submit( - message_generator.create_successor_function, - self._prefix, - message, - sequence_fields, - ), self._executor.submit( message_generator.create_invalid_successor_function, message, diff --git a/rflx/generator/message.py b/rflx/generator/message.py index 2c8f4cb5b..991036959 100644 --- a/rflx/generator/message.py +++ b/rflx/generator/message.py @@ -2220,76 +2220,6 @@ def condition(field: Field, message: Message) -> Expr: ) -def create_successor_function( - prefix: str, - message: Message, - sequence_fields: abc.Mapping[Field, Type], -) -> UnitPart: - if ( - len(sequence_fields) == 0 - and len([t for t in message.field_types.values() if isinstance(t, (Opaque, Sequence))]) == 0 - ): - return UnitPart() - specification = FunctionSpecification( - "Successor", - "Virtual_Field", - [Parameter(["Ctx"], "Context"), Parameter(["Fld"], "Field")], - ) - - return UnitPart( - [], - common.wrap_warning( - [ - ExpressionFunctionDeclaration( - specification, - Case( - Variable("Fld"), - [ - ( - Variable(f.affixed_name), - If( - [ - ( - l.condition.substituted( - common.substitution(message, prefix), - ) - .simplified() - .ada_expr(), - Variable(l.target.affixed_name), - ) - for l in message.outgoing(f) - ], - Variable(INITIAL.affixed_name), - ), - ) - for f in message.fields - ], - ), - [ - Precondition( - And( - Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]), - Call( - prefix * message.identifier * "Well_Formed", - [Variable("Ctx"), Variable("Fld")], - ), - Call( - prefix * message.identifier * "Valid_Next", - [Variable("Ctx"), Variable("Fld")], - ), - ), - ), - ], - ), - ], - [ - # Eng/RecordFlux/Workarounds#31 - "precondition is always False", - ], - ), - ) - - def create_invalid_successor_function(message: Message, requires_set_procedure: bool) -> UnitPart: if len(message.fields) == 1 or not requires_set_procedure: return UnitPart() diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb index 5e8d6f0b0..172545b8b 100644 --- a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb +++ b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb @@ -67,20 +67,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Data => - F_Final)) - with - Pre => - RFLX.Test.Message.Has_Buffer (Ctx) - and RFLX.Test.Message.Well_Formed (Ctx, Fld) - and RFLX.Test.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last @@ -271,7 +257,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context; Length : RFLX_Types.Length) is diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.adb b/tests/feature/parameterized_messages/generated/rflx-test-message.adb index 31b7e0469..fb03d7985 100644 --- a/tests/feature/parameterized_messages/generated/rflx-test-message.adb +++ b/tests/feature/parameterized_messages/generated/rflx-test-message.adb @@ -67,31 +67,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Data => - (if - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - then - F_Extension - elsif - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (False)) - then - F_Final - else - F_Initial), - when F_Extension => - F_Final)) - with - Pre => - RFLX.Test.Message.Has_Buffer (Ctx) - and RFLX.Test.Message.Well_Formed (Ctx, Fld) - and RFLX.Test.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last @@ -258,7 +233,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context) is @@ -297,7 +271,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Extension) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Extension)) := (State => S_Invalid, others => <>); end Initialize_Extension_Private; procedure Initialize_Extension (Ctx : in out Context) is diff --git a/tests/feature/session_functions/generated/rflx-test-definite_message.adb b/tests/feature/session_functions/generated/rflx-test-definite_message.adb index 09448a55b..9c1c06949 100644 --- a/tests/feature/session_functions/generated/rflx-test-definite_message.adb +++ b/tests/feature/session_functions/generated/rflx-test-definite_message.adb @@ -68,24 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Message_Type => - F_Length, - when F_Length => - F_Data, - when F_Data => - F_Final)) - with - Pre => - RFLX.Test.Definite_Message.Has_Buffer (Ctx) - and RFLX.Test.Definite_Message.Well_Formed (Ctx, Fld) - and RFLX.Test.Definite_Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Message_Type => @@ -396,7 +378,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context) is diff --git a/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb b/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb index 763d98292..068f1185c 100644 --- a/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb +++ b/tests/feature/session_message_optimization/generated/rflx-test-option_data.adb @@ -68,22 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Length => - (if Ctx.Cursors (F_Length).Value > 1 then F_Data else F_Initial), - when F_Data => - F_Final)) - with - Pre => - RFLX.Test.Option_Data.Has_Buffer (Ctx) - and RFLX.Test.Option_Data.Well_Formed (Ctx, Fld) - and RFLX.Test.Option_Data.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Length => @@ -353,7 +337,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context) is diff --git a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb index 50d1364cb..22f79f2a4 100644 --- a/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb +++ b/tests/feature/session_sequence_append_head/generated/rflx-tlv-message.adb @@ -68,33 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Tag => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Error)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Data)) - then - F_Length - else - F_Initial), - when F_Length => - F_Value, - when F_Value => - F_Final)) - with - Pre => - RFLX.TLV.Message.Has_Buffer (Ctx) - and RFLX.TLV.Message.Well_Formed (Ctx, Fld) - and RFLX.TLV.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Tag => @@ -384,7 +357,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Value) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, others => <>); end Initialize_Value_Private; procedure Initialize_Value (Ctx : in out Context) is diff --git a/tests/feature/shared/generated/rflx-universal-message.adb b/tests/feature/shared/generated/rflx-universal-message.adb index 0813ee7a7..93030f517 100644 --- a/tests/feature/shared/generated/rflx-universal-message.adb +++ b/tests/feature/shared/generated/rflx-universal-message.adb @@ -68,65 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Message_Type => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data)) - then - F_Data - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Null)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) /= RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options)) - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) /= RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Null)) - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) /= RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Data)) - then - F_Length - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Unconstrained_Options)) - then - F_Options - else - F_Initial), - when F_Length => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Data)) - then - F_Data - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Option_Types)) - then - F_Option_Types - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Options)) - then - F_Options - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Value)) - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Length).Value) = Universal.Value'Size / 8 - then - F_Value - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.MT_Values)) - then - F_Values - else - F_Initial), - when F_Data | F_Option_Types | F_Options | F_Value | F_Values => - F_Final)) - with - Pre => - RFLX.Universal.Message.Has_Buffer (Ctx) - and RFLX.Universal.Message.Well_Formed (Ctx, Fld) - and RFLX.Universal.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Message_Type => @@ -496,7 +437,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context; Length : RFLX_Types.Length) is @@ -538,7 +478,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Option_Types) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Option_Types)) := (State => S_Invalid, others => <>); end Initialize_Option_Types_Private; procedure Initialize_Option_Types (Ctx : in out Context) is @@ -578,7 +517,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Options) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, others => <>); end Initialize_Options_Private; procedure Initialize_Options (Ctx : in out Context; Length : RFLX_Types.Length) is @@ -617,7 +555,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Values) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Values)) := (State => S_Invalid, others => <>); end Initialize_Values_Private; procedure Initialize_Values (Ctx : in out Context) is @@ -655,7 +592,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Option_Types) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Option_Types)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); @@ -674,7 +610,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Options) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); @@ -693,7 +628,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Values) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Values)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); diff --git a/tests/feature/shared/generated/rflx-universal-option.adb b/tests/feature/shared/generated/rflx-universal-option.adb index 945d08819..0c3a23695 100644 --- a/tests/feature/shared/generated/rflx-universal-option.adb +++ b/tests/feature/shared/generated/rflx-universal-option.adb @@ -68,33 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Option_Type => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.OT_Null)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.OT_Data)) - then - F_Length - else - F_Initial), - when F_Length => - F_Data, - when F_Data => - F_Final)) - with - Pre => - RFLX.Universal.Option.Has_Buffer (Ctx) - and RFLX.Universal.Option.Well_Formed (Ctx, Fld) - and RFLX.Universal.Option.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Option_Type => @@ -389,7 +362,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-derivation-message.adb b/tests/spark/generated/rflx-derivation-message.adb index 4cd499968..823e161ab 100644 --- a/tests/spark/generated/rflx-derivation-message.adb +++ b/tests/spark/generated/rflx-derivation-message.adb @@ -68,33 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Tag => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Error)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Data)) - then - F_Length - else - F_Initial), - when F_Length => - F_Value, - when F_Value => - F_Final)) - with - Pre => - RFLX.Derivation.Message.Has_Buffer (Ctx) - and RFLX.Derivation.Message.Well_Formed (Ctx, Fld) - and RFLX.Derivation.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Tag => @@ -389,7 +362,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Value) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, others => <>); end Initialize_Value_Private; procedure Initialize_Value (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-ethernet-frame.adb b/tests/spark/generated/rflx-ethernet-frame.adb index 8ee6173bf..f976c40e6 100644 --- a/tests/spark/generated/rflx-ethernet-frame.adb +++ b/tests/spark/generated/rflx-ethernet-frame.adb @@ -68,56 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Destination => - F_Source, - when F_Source => - F_Type_Length_TPID, - when F_Type_Length_TPID => - (if - Ctx.Cursors (F_Type_Length_TPID).Value = 16#8100# - then - F_TPID - elsif - Ctx.Cursors (F_Type_Length_TPID).Value /= 16#8100# - then - F_Type_Length - else - F_Initial), - when F_TPID => - F_TCI, - when F_TCI => - F_Type_Length, - when F_Type_Length => - (if - Ctx.Cursors (F_Type_Length).Value <= 1500 - then - F_Payload - elsif - Ctx.Cursors (F_Type_Length).Value >= 1536 - then - F_Payload - else - F_Initial), - when F_Payload => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1) / 8 >= 46 - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1) / 8 <= 1500 - then - F_Final - else - F_Initial))) - with - Pre => - RFLX.Ethernet.Frame.Has_Buffer (Ctx) - and RFLX.Ethernet.Frame.Well_Formed (Ctx, Fld) - and RFLX.Ethernet.Frame.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Destination => @@ -431,7 +381,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Payload) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, others => <>); end Initialize_Payload_Private; procedure Initialize_Payload (Ctx : in out Context; Length : RFLX_Types.Length) is diff --git a/tests/spark/generated/rflx-expression-message.adb b/tests/spark/generated/rflx-expression-message.adb index 74f996901..31a7fe203 100644 --- a/tests/spark/generated/rflx-expression-message.adb +++ b/tests/spark/generated/rflx-expression-message.adb @@ -67,25 +67,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Payload => - (if - Equal (Ctx, F_Payload, (RFLX_Types.Byte'Val (1), RFLX_Types.Byte'Val (2))) - then - F_Final - else - F_Initial))) - with - Pre => - RFLX.Expression.Message.Has_Buffer (Ctx) - and RFLX.Expression.Message.Well_Formed (Ctx, Fld) - and RFLX.Expression.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last @@ -217,7 +198,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Payload) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, others => <>); end Initialize_Payload_Private; procedure Initialize_Payload (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.adb b/tests/spark/generated/rflx-fixed_size-simple_message.adb index e765001c6..b8f247a24 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.adb +++ b/tests/spark/generated/rflx-fixed_size-simple_message.adb @@ -68,27 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Message_Type => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Message_Type).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.Universal.OT_Data)) - then - F_Data - else - F_Initial), - when F_Data => - F_Final)) - with - Pre => - RFLX.Fixed_Size.Simple_Message.Has_Buffer (Ctx) - and RFLX.Fixed_Size.Simple_Message.Well_Formed (Ctx, Fld) - and RFLX.Fixed_Size.Simple_Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Message_Type => @@ -386,7 +365,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-icmp-message.adb b/tests/spark/generated/rflx-icmp-message.adb index f69e48b7c..9ca2b952c 100644 --- a/tests/spark/generated/rflx-icmp-message.adb +++ b/tests/spark/generated/rflx-icmp-message.adb @@ -68,108 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Tag => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Destination_Unreachable)) - then - F_Code_Destination_Unreachable - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Redirect)) - then - F_Code_Redirect - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Time_Exceeded)) - then - F_Code_Time_Exceeded - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Request)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Msg)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Parameter_Problem)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Source_Quench)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Request)) - then - F_Code_Zero - else - F_Initial), - when F_Code_Destination_Unreachable | F_Code_Redirect | F_Code_Time_Exceeded | F_Code_Zero => - F_Checksum, - when F_Checksum => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Redirect)) - then - F_Gateway_Internet_Address - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Request)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Msg)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Request)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Reply)) - then - F_Identifier - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Parameter_Problem)) - then - F_Pointer - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Time_Exceeded)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Destination_Unreachable)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Source_Quench)) - then - F_Unused_32 - else - F_Initial), - when F_Gateway_Internet_Address => - F_Data, - when F_Identifier => - F_Sequence_Number, - when F_Pointer => - F_Unused_24, - when F_Unused_32 => - F_Data, - when F_Sequence_Number => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Reply)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Echo_Request)) - then - F_Data - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Request)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Information_Reply)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Msg)) - or else RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.ICMP.Timestamp_Reply)) - then - F_Originate_Timestamp - else - F_Initial), - when F_Unused_24 => - F_Data, - when F_Originate_Timestamp => - F_Receive_Timestamp, - when F_Data => - F_Final, - when F_Receive_Timestamp => - F_Transmit_Timestamp, - when F_Transmit_Timestamp => - F_Final)) - with - Pre => - RFLX.ICMP.Message.Has_Buffer (Ctx) - and RFLX.ICMP.Message.Well_Formed (Ctx, Fld) - and RFLX.ICMP.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Tag => @@ -572,7 +470,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, others => <>); end Initialize_Data_Private; procedure Initialize_Data (Ctx : in out Context; Length : RFLX_Types.Length) is diff --git a/tests/spark/generated/rflx-ipv4-option.adb b/tests/spark/generated/rflx-ipv4-option.adb index e44278819..5d7940e32 100644 --- a/tests/spark/generated/rflx-ipv4-option.adb +++ b/tests/spark/generated/rflx-ipv4-option.adb @@ -68,54 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Copied => - F_Option_Class, - when F_Option_Class => - F_Option_Number, - when F_Option_Number => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Class).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.IPv4.Control)) - and then Ctx.Cursors (F_Option_Number).Value = 1 - then - F_Final - elsif - Ctx.Cursors (F_Option_Number).Value > 1 - then - F_Option_Length - else - F_Initial), - when F_Option_Length => - (if - (RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Class).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.IPv4.Debugging_And_Measurement)) - and then Ctx.Cursors (F_Option_Number).Value = 4) - or else (RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Class).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.IPv4.Control)) - and then (Ctx.Cursors (F_Option_Number).Value = 9 - or else Ctx.Cursors (F_Option_Number).Value = 3 - or else Ctx.Cursors (F_Option_Number).Value = 7)) - or else (Ctx.Cursors (F_Option_Length).Value = 11 - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Class).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.IPv4.Control)) - and then Ctx.Cursors (F_Option_Number).Value = 2) - or else (Ctx.Cursors (F_Option_Length).Value = 4 - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_Option_Class).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.IPv4.Control)) - and then Ctx.Cursors (F_Option_Number).Value = 8) - then - F_Option_Data - else - F_Initial), - when F_Option_Data => - F_Final)) - with - Pre => - RFLX.IPv4.Option.Has_Buffer (Ctx) - and RFLX.IPv4.Option.Well_Formed (Ctx, Fld) - and RFLX.IPv4.Option.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Copied => @@ -429,7 +381,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Option_Data) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Option_Data)) := (State => S_Invalid, others => <>); end Initialize_Option_Data_Private; procedure Initialize_Option_Data (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-ipv4-packet.adb b/tests/spark/generated/rflx-ipv4-packet.adb index 424a100c2..783bea689 100644 --- a/tests/spark/generated/rflx-ipv4-packet.adb +++ b/tests/spark/generated/rflx-ipv4-packet.adb @@ -68,62 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Version => - F_IHL, - when F_IHL => - F_DSCP, - when F_DSCP => - F_ECN, - when F_ECN => - F_Total_Length, - when F_Total_Length => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Total_Length).Value) >= RFLX_Types.Base_Integer (Ctx.Cursors (F_IHL).Value) * 4 - then - F_Identification - else - F_Initial), - when F_Identification => - F_Flag_R, - when F_Flag_R => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Flag_R).Value) = RFLX_Types.Base_Integer (To_Base_Integer (False)) - then - F_Flag_DF - else - F_Initial), - when F_Flag_DF => - F_Flag_MF, - when F_Flag_MF => - F_Fragment_Offset, - when F_Fragment_Offset => - F_TTL, - when F_TTL => - F_Protocol, - when F_Protocol => - F_Header_Checksum, - when F_Header_Checksum => - F_Source, - when F_Source => - F_Destination, - when F_Destination => - F_Options, - when F_Options => - F_Payload, - when F_Payload => - F_Final)) - with - Pre => - RFLX.IPv4.Packet.Has_Buffer (Ctx) - and RFLX.IPv4.Packet.Well_Formed (Ctx, Fld) - and RFLX.IPv4.Packet.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Version => @@ -551,7 +495,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Options) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, others => <>); end Initialize_Options_Private; procedure Initialize_Options (Ctx : in out Context) is @@ -602,7 +545,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Payload) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, others => <>); end Initialize_Payload_Private; procedure Initialize_Payload (Ctx : in out Context) is @@ -640,7 +582,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Options) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); diff --git a/tests/spark/generated/rflx-sequence-inner_message.adb b/tests/spark/generated/rflx-sequence-inner_message.adb index 25621e984..b30383976 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.adb +++ b/tests/spark/generated/rflx-sequence-inner_message.adb @@ -68,22 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Length => - F_Payload, - when F_Payload => - F_Final)) - with - Pre => - RFLX.Sequence.Inner_Message.Has_Buffer (Ctx) - and RFLX.Sequence.Inner_Message.Well_Formed (Ctx, Fld) - and RFLX.Sequence.Inner_Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Length => @@ -368,7 +352,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Payload) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, others => <>); end Initialize_Payload_Private; procedure Initialize_Payload (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-sequence-message.adb b/tests/spark/generated/rflx-sequence-message.adb index 0ca350dd9..9060da004 100644 --- a/tests/spark/generated/rflx-sequence-message.adb +++ b/tests/spark/generated/rflx-sequence-message.adb @@ -68,26 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Length => - F_Integer_Vector, - when F_Integer_Vector => - F_Enumeration_Vector, - when F_Enumeration_Vector => - F_AV_Enumeration_Vector, - when F_AV_Enumeration_Vector => - F_Final)) - with - Pre => - RFLX.Sequence.Message.Has_Buffer (Ctx) - and RFLX.Sequence.Message.Well_Formed (Ctx, Fld) - and RFLX.Sequence.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Length => @@ -387,7 +367,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Integer_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Integer_Vector)) := (State => S_Invalid, others => <>); end Initialize_Integer_Vector_Private; procedure Initialize_Integer_Vector (Ctx : in out Context) is @@ -427,7 +406,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Enumeration_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Enumeration_Vector)) := (State => S_Invalid, others => <>); end Initialize_Enumeration_Vector_Private; procedure Initialize_Enumeration_Vector (Ctx : in out Context) is @@ -465,7 +443,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_AV_Enumeration_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_AV_Enumeration_Vector)) := (State => S_Invalid, others => <>); end Initialize_AV_Enumeration_Vector_Private; procedure Initialize_AV_Enumeration_Vector (Ctx : in out Context) is @@ -484,7 +461,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Integer_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Integer_Vector)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); @@ -503,7 +479,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Enumeration_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Enumeration_Vector)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); @@ -522,7 +497,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_AV_Enumeration_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_AV_Enumeration_Vector)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); diff --git a/tests/spark/generated/rflx-sequence-messages_message.adb b/tests/spark/generated/rflx-sequence-messages_message.adb index 582e9e695..ecb27328f 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.adb +++ b/tests/spark/generated/rflx-sequence-messages_message.adb @@ -68,22 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Length => - F_Messages, - when F_Messages => - F_Final)) - with - Pre => - RFLX.Sequence.Messages_Message.Has_Buffer (Ctx) - and RFLX.Sequence.Messages_Message.Well_Formed (Ctx, Fld) - and RFLX.Sequence.Messages_Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Length => @@ -356,7 +340,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Messages) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Messages)) := (State => S_Invalid, others => <>); end Initialize_Messages_Private; procedure Initialize_Messages (Ctx : in out Context) is @@ -375,7 +358,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Messages) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Messages)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb index 30daf725d..b82ef4cae 100644 --- a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb +++ b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb @@ -68,22 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Header => - F_Vector, - when F_Vector => - F_Final)) - with - Pre => - RFLX.Sequence.Sequence_Size_Defined_By_Message_Size.Has_Buffer (Ctx) - and RFLX.Sequence.Sequence_Size_Defined_By_Message_Size.Well_Formed (Ctx, Fld) - and RFLX.Sequence.Sequence_Size_Defined_By_Message_Size.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Header => @@ -356,7 +340,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Vector)) := (State => S_Invalid, others => <>); end Initialize_Vector_Private; procedure Initialize_Vector (Ctx : in out Context; Length : RFLX_Types.Length) is @@ -375,7 +358,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => RFLX_Types.Bit_Length'Max (Ctx.Written_Last, Last)); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Vector) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Vector)) := (State => S_Invalid, others => <>); end if; Take_Buffer (Ctx, Buffer); pragma Warnings (Off, "unused assignment to ""Buffer"""); diff --git a/tests/spark/generated/rflx-tlv-message.adb b/tests/spark/generated/rflx-tlv-message.adb index 50d1364cb..22f79f2a4 100644 --- a/tests/spark/generated/rflx-tlv-message.adb +++ b/tests/spark/generated/rflx-tlv-message.adb @@ -68,33 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Tag => - (if - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Error)) - then - F_Final - elsif - RFLX_Types.Base_Integer (Ctx.Cursors (F_Tag).Value) = RFLX_Types.Base_Integer (To_Base_Integer (RFLX.TLV.Msg_Data)) - then - F_Length - else - F_Initial), - when F_Length => - F_Value, - when F_Value => - F_Final)) - with - Pre => - RFLX.TLV.Message.Has_Buffer (Ctx) - and RFLX.TLV.Message.Well_Formed (Ctx, Fld) - and RFLX.TLV.Message.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Tag => @@ -384,7 +357,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Value) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, others => <>); end Initialize_Value_Private; procedure Initialize_Value (Ctx : in out Context) is diff --git a/tests/spark/generated/rflx-udp-datagram.adb b/tests/spark/generated/rflx-udp-datagram.adb index 4bc05b28e..f3f14376c 100644 --- a/tests/spark/generated/rflx-udp-datagram.adb +++ b/tests/spark/generated/rflx-udp-datagram.adb @@ -68,28 +68,6 @@ is Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); end Data; - pragma Warnings (Off, "precondition is always False"); - - function Successor (Ctx : Context; Fld : Field) return Virtual_Field is - ((case Fld is - when F_Source_Port => - F_Destination_Port, - when F_Destination_Port => - F_Length, - when F_Length => - F_Checksum, - when F_Checksum => - F_Payload, - when F_Payload => - F_Final)) - with - Pre => - RFLX.UDP.Datagram.Has_Buffer (Ctx) - and RFLX.UDP.Datagram.Well_Formed (Ctx, Fld) - and RFLX.UDP.Datagram.Valid_Next (Ctx, Fld); - - pragma Warnings (On, "precondition is always False"); - function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Source_Port => @@ -393,7 +371,6 @@ is Ctx := Ctx'Update (Verified_Last => Last, Written_Last => Last); pragma Warnings (On, "attribute Update is an obsolescent feature"); Ctx.Cursors (F_Payload) := (State => S_Well_Formed, First => First, Last => Last, Value => 0); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, others => <>); end Initialize_Payload_Private; procedure Initialize_Payload (Ctx : in out Context) is