diff --git a/CHANGELOG.md b/CHANGELOG.md index 943a4e70a..df1894b8f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,6 +27,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changed - Remove unused `Buffer` arguments in generated code (eng/recordflux/RecordFlux#1802) +- Remove unnecessary part of `Valid_Context` predicate (eng/recordflux/RecordFlux#1802) ## [0.24.0] - 2024-09-12 diff --git a/examples/apps/spdm_responder/build_lib.gpr b/examples/apps/spdm_responder/build_lib.gpr index ca66a2195..5ea9e3abb 100644 --- a/examples/apps/spdm_responder/build_lib.gpr +++ b/examples/apps/spdm_responder/build_lib.gpr @@ -107,7 +107,7 @@ project Build_Lib is package Prove is for Proof_Switches ("Ada") use Defaults.Proof_Switches; for Proof_Switches ("responder.adb") use ("--prover=z3,cvc5", "--steps=64000", "--memlimit=6000", "--timeout=600"); - for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=240"); + for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=240", "--memlimit=3000"); end Prove; end Build_Lib; diff --git a/rflx/generator/common.py b/rflx/generator/common.py index 84ea07952..6de83b9e6 100644 --- a/rflx/generator/common.py +++ b/rflx/generator/common.py @@ -486,39 +486,6 @@ def context_predicate( message: model.Message, prefix: str, ) -> Expr: - def invalid_successors_invariant() -> Expr: - """ - Create the invariant that defines the state of successors of invalid fields. - - This invariant ensures for all invalid message fields that all its successor fields are also - invalid. - """ - return AndThen( - *[ - IfThenElse( - AndThen( - *[ - Call( - "Invalid", - [Indexed(Variable("Cursors"), Variable(p.affixed_name))], - ) - for p in message.direct_predecessors(f) - ], - ), - Call( - "Invalid", - [ - Indexed( - Variable("Cursors"), - Variable(f.affixed_name), - ), - ], - ), - ) - for f in message.fields - if f not in message.direct_successors(model.INITIAL) - ], - ) return AndThen( IfThenElse( @@ -553,7 +520,6 @@ def invalid_successors_invariant() -> Expr: *[Variable(p.identifier) for p in message.parameter_types], ], ), - invalid_successors_invariant(), message_structure_invariant(message, prefix, embedded=True), ) diff --git a/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads b/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads index 63a58b0a7..30d21e7b3 100644 --- a/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads +++ b/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads @@ -601,7 +601,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then (True) and then ((if Well_Formed (Cursors (F_Value)) then diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads index 4824311e1..ec4a036ed 100644 --- a/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads +++ b/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads @@ -649,7 +649,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B)))) and then ((if Well_Formed (Cursors (F_A)) then diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads index b78dcc346..e842b2c88 100644 --- a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads +++ b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads @@ -649,7 +649,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_C)) then Invalid (Cursors (F_D)))) and then ((if Well_Formed (Cursors (F_C)) then diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads index 290135e1f..e316074b1 100644 --- a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads +++ b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads @@ -699,8 +699,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_X_A)) then Invalid (Cursors (F_X_B))) - and then (if Invalid (Cursors (F_X_B)) then Invalid (Cursors (F_Y)))) and then ((if Well_Formed (Cursors (F_X_A)) then diff --git a/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads b/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads index 3a29f97b5..60a1ee4e9 100644 --- a/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads +++ b/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads @@ -808,8 +808,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data)))) and then ((if Well_Formed (Cursors (F_Message_Type)) then diff --git a/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads b/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads index 13f49625a..276ab752e 100644 --- a/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads +++ b/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads @@ -740,7 +740,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data)))) and then ((if Well_Formed (Cursors (F_Length)) then diff --git a/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads b/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads index 3c85c922b..290dc6d83 100644 --- a/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads +++ b/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads @@ -775,8 +775,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value)))) and then ((if Well_Formed (Cursors (F_Tag)) then diff --git a/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads b/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads index 7d861b550..87c0043c8 100644 --- a/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads +++ b/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads @@ -798,8 +798,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) - and then ((if Invalid (Cursors (F_Has_Data)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data)))) and then ((if Well_Formed (Cursors (F_Has_Data)) then diff --git a/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads b/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads index 5cfdfbc2e..0058d98cf 100644 --- a/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads +++ b/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads @@ -654,7 +654,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B)))) and then ((if Well_Formed (Cursors (F_A)) then diff --git a/tests/feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads b/tests/feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads index c966ec095..9be0d4833 100644 --- a/tests/feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads +++ b/tests/feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads @@ -653,7 +653,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B)))) and then ((if Well_Formed (Cursors (F_A)) then 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 364eaef3b..2457d2176 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 @@ -633,7 +633,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, P) - and then (True) and then ((if Well_Formed (Cursors (F_F1)) then 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 176526093..c41289427 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 @@ -664,7 +664,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then (True) and then ((if Well_Formed (Cursors (F_Data)) then diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads index f5b2864d1..2db1de016 100644 --- a/tests/feature/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/feature/parameterized_messages/generated/rflx-test-message.ads @@ -773,7 +773,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Length, Extended) - and then ((if Invalid (Cursors (F_Data)) then Invalid (Cursors (F_Extension)))) and then ((if Well_Formed (Cursors (F_Data)) then diff --git a/tests/feature/shared/generated/rflx-universal-message.ads b/tests/feature/shared/generated/rflx-universal-message.ads index e694ef5d1..c76f4de44 100644 --- a/tests/feature/shared/generated/rflx-universal-message.ads +++ b/tests/feature/shared/generated/rflx-universal-message.ads @@ -1440,20 +1440,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length))) - and then (if - Invalid (Cursors (F_Length)) - and then Invalid (Cursors (F_Message_Type)) - then - Invalid (Cursors (F_Data))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Option_Types))) - and then (if - Invalid (Cursors (F_Length)) - and then Invalid (Cursors (F_Message_Type)) - then - Invalid (Cursors (F_Options))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Values)))) and then ((if Well_Formed (Cursors (F_Message_Type)) then diff --git a/tests/feature/shared/generated/rflx-universal-option.ads b/tests/feature/shared/generated/rflx-universal-option.ads index 70795865e..f69046da1 100644 --- a/tests/feature/shared/generated/rflx-universal-option.ads +++ b/tests/feature/shared/generated/rflx-universal-option.ads @@ -775,8 +775,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Option_Type)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data)))) and then ((if Well_Formed (Cursors (F_Option_Type)) then diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index 6862625f7..328ac34e3 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -777,8 +777,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value)))) and then ((if Well_Formed (Cursors (F_Tag)) then diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads index e6b35a2d9..b630319be 100644 --- a/tests/spark/generated/rflx-enumeration-message.ads +++ b/tests/spark/generated/rflx-enumeration-message.ads @@ -601,7 +601,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then (True) and then ((if Well_Formed (Cursors (F_Priority)) then diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index 3f17637d9..3bfce867f 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -989,16 +989,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Destination)) then Invalid (Cursors (F_Source))) - and then (if Invalid (Cursors (F_Source)) then Invalid (Cursors (F_Type_Length_TPID))) - and then (if Invalid (Cursors (F_Type_Length_TPID)) then Invalid (Cursors (F_TPID))) - and then (if Invalid (Cursors (F_TPID)) then Invalid (Cursors (F_TCI))) - and then (if - Invalid (Cursors (F_TCI)) - and then Invalid (Cursors (F_Type_Length_TPID)) - then - Invalid (Cursors (F_Type_Length))) - and then (if Invalid (Cursors (F_Type_Length)) then Invalid (Cursors (F_Payload)))) and then ((if Well_Formed (Cursors (F_Destination)) then diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index edfe07b28..01ec3ef43 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.ads @@ -673,7 +673,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) - and then (True) and then ((if Well_Formed (Cursors (F_Payload)) then diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 76bca12d8..8c001332c 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -743,7 +743,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Data)))) and then ((if Well_Formed (Cursors (F_Message_Type)) then diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index 161d822da..e23e38926 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -1637,33 +1637,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Destination_Unreachable))) - and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Redirect))) - and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Time_Exceeded))) - and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Zero))) - and then (if - Invalid (Cursors (F_Code_Destination_Unreachable)) - and then Invalid (Cursors (F_Code_Redirect)) - and then Invalid (Cursors (F_Code_Time_Exceeded)) - and then Invalid (Cursors (F_Code_Zero)) - then - Invalid (Cursors (F_Checksum))) - and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Gateway_Internet_Address))) - and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Identifier))) - and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Pointer))) - and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Unused_32))) - and then (if Invalid (Cursors (F_Identifier)) then Invalid (Cursors (F_Sequence_Number))) - and then (if Invalid (Cursors (F_Pointer)) then Invalid (Cursors (F_Unused_24))) - and then (if Invalid (Cursors (F_Sequence_Number)) then Invalid (Cursors (F_Originate_Timestamp))) - and then (if - Invalid (Cursors (F_Gateway_Internet_Address)) - and then Invalid (Cursors (F_Sequence_Number)) - and then Invalid (Cursors (F_Unused_24)) - and then Invalid (Cursors (F_Unused_32)) - then - Invalid (Cursors (F_Data))) - and then (if Invalid (Cursors (F_Originate_Timestamp)) then Invalid (Cursors (F_Receive_Timestamp))) - and then (if Invalid (Cursors (F_Receive_Timestamp)) then Invalid (Cursors (F_Transmit_Timestamp)))) and then ((if Well_Formed (Cursors (F_Tag)) then diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index e9edae83a..34a4551c3 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -920,10 +920,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Copied)) then Invalid (Cursors (F_Option_Class))) - and then (if Invalid (Cursors (F_Option_Class)) then Invalid (Cursors (F_Option_Number))) - and then (if Invalid (Cursors (F_Option_Number)) then Invalid (Cursors (F_Option_Length))) - and then (if Invalid (Cursors (F_Option_Length)) then Invalid (Cursors (F_Option_Data)))) and then ((if Well_Formed (Cursors (F_Copied)) then diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index 7d882bece..12885068e 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -1803,22 +1803,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Version)) then Invalid (Cursors (F_IHL))) - and then (if Invalid (Cursors (F_IHL)) then Invalid (Cursors (F_DSCP))) - and then (if Invalid (Cursors (F_DSCP)) then Invalid (Cursors (F_ECN))) - and then (if Invalid (Cursors (F_ECN)) then Invalid (Cursors (F_Total_Length))) - and then (if Invalid (Cursors (F_Total_Length)) then Invalid (Cursors (F_Identification))) - and then (if Invalid (Cursors (F_Identification)) then Invalid (Cursors (F_Flag_R))) - and then (if Invalid (Cursors (F_Flag_R)) then Invalid (Cursors (F_Flag_DF))) - and then (if Invalid (Cursors (F_Flag_DF)) then Invalid (Cursors (F_Flag_MF))) - and then (if Invalid (Cursors (F_Flag_MF)) then Invalid (Cursors (F_Fragment_Offset))) - and then (if Invalid (Cursors (F_Fragment_Offset)) then Invalid (Cursors (F_TTL))) - and then (if Invalid (Cursors (F_TTL)) then Invalid (Cursors (F_Protocol))) - and then (if Invalid (Cursors (F_Protocol)) then Invalid (Cursors (F_Header_Checksum))) - and then (if Invalid (Cursors (F_Header_Checksum)) then Invalid (Cursors (F_Source))) - and then (if Invalid (Cursors (F_Source)) then Invalid (Cursors (F_Destination))) - and then (if Invalid (Cursors (F_Destination)) then Invalid (Cursors (F_Options))) - and then (if Invalid (Cursors (F_Options)) then Invalid (Cursors (F_Payload)))) and then ((if Well_Formed (Cursors (F_Version)) then diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index fe728c270..7880a4fec 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -753,7 +753,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Payload)))) and then ((if Well_Formed (Cursors (F_Length)) then diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index 45550f6e1..198b70ce7 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -1014,9 +1014,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Integer_Vector))) - and then (if Invalid (Cursors (F_Integer_Vector)) then Invalid (Cursors (F_Enumeration_Vector))) - and then (if Invalid (Cursors (F_Enumeration_Vector)) then Invalid (Cursors (F_AV_Enumeration_Vector)))) and then ((if Well_Formed (Cursors (F_Length)) then diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index 806993645..a20b7bed9 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -738,7 +738,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Messages)))) and then ((if Well_Formed (Cursors (F_Length)) then 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 754b83387..e5bffdfed 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 @@ -740,7 +740,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Header)) then Invalid (Cursors (F_Vector)))) and then ((if Well_Formed (Cursors (F_Header)) then diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index 3c85c922b..290dc6d83 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/generated/rflx-tlv-message.ads @@ -775,8 +775,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value)))) and then ((if Well_Formed (Cursors (F_Tag)) then diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index f577c64b1..bfa9a143e 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -918,10 +918,6 @@ private and then Written_Last rem RFLX_Types.Byte'Size = 0 and then Cursors_Invariant (Cursors, First, Verified_Last) and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last) - and then ((if Invalid (Cursors (F_Source_Port)) then Invalid (Cursors (F_Destination_Port))) - and then (if Invalid (Cursors (F_Destination_Port)) then Invalid (Cursors (F_Length))) - and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Checksum))) - and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Payload)))) and then ((if Well_Formed (Cursors (F_Source_Port)) then