From 0e17ad214dd9db6281177f28f86720c1ad757f78 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Mon, 20 Dec 2021 17:40:00 +0100 Subject: [PATCH] Improve provability Ref. #736 --- rflx/generator/generator.py | 39 +++++++++++++++++-- rflx/generator/parser.py | 28 ++++++++++++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-test-message.ads | 6 ++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../rflx-fixed_size-simple_message.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-tlv-message.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-universal-message.adb | 13 ++++++- .../generated/rflx-universal-message.ads | 8 +++- .../generated/rflx-universal-option.ads | 8 +++- .../generated/rflx-derivation-message.ads | 8 +++- tests/spark/generated/rflx-ethernet-frame.ads | 8 +++- .../generated/rflx-expression-message.ads | 6 ++- .../rflx-fixed_size-simple_message.ads | 8 +++- tests/spark/generated/rflx-icmp-message.ads | 8 +++- tests/spark/generated/rflx-ipv4-option.ads | 8 +++- tests/spark/generated/rflx-ipv4-packet.adb | 9 ++++- tests/spark/generated/rflx-ipv4-packet.ads | 8 +++- .../generated/rflx-sequence-inner_message.ads | 8 +++- .../spark/generated/rflx-sequence-message.adb | 13 ++++++- .../spark/generated/rflx-sequence-message.ads | 8 +++- .../rflx-sequence-messages_message.ads | 8 +++- ...-sequence_size_defined_by_message_size.ads | 8 +++- tests/spark/generated/rflx-tlv-message.ads | 8 +++- tests/spark/generated/rflx-udp-datagram.ads | 8 +++- 68 files changed, 607 insertions(+), 70 deletions(-) diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py index 8681c45b2..0ff96b39b 100644 --- a/rflx/generator/generator.py +++ b/rflx/generator/generator.py @@ -403,7 +403,7 @@ def __create_message(self, message: Message) -> None: unit += self.__create_field_condition_function(message) unit += self.__create_field_size_function(message, scalar_fields, composite_fields) unit += self.__create_field_first_function(message) - unit += self.__create_field_last_function() + unit += self.__create_field_last_function(scalar_fields, composite_fields) unit += self.__create_predecessor_function() unit += self.__create_successor_function(message) unit += self.__create_valid_predecessor_function(message, composite_fields) @@ -1891,7 +1891,9 @@ def substituted( ) @staticmethod - def __create_field_last_function() -> UnitPart: + def __create_field_last_function( + scalar_fields: ty.Mapping[Field, Type], composite_fields: ty.Sequence[Field] + ) -> UnitPart: specification = FunctionSpecification( "Field_Last", const.TYPES_BIT_INDEX, @@ -1911,7 +1913,38 @@ def __create_field_last_function() -> UnitPart: Call("Field_Size", [Variable("Ctx"), Variable("Fld")]), ), ) - ) + ), + *( + [ + Postcondition( + Case( + Variable("Fld"), + [ + *[ + ( + Variable(f.affixed_name), + Equal( + Mod( + Result("Field_Last"), + Size(const.TYPES_BYTE), + ), + Number(0), + ), + ) + for f in composite_fields + ], + *( + [(Variable("others"), TRUE)] + if scalar_fields + else [] + ), + ], + ) + ) + ] + if composite_fields + else [] + ), ], ) ], diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py index 3ce91deb5..7e181b421 100644 --- a/rflx/generator/parser.py +++ b/rflx/generator/parser.py @@ -34,6 +34,7 @@ Mod, Mul, NamedAggregate, + NullStatement, Number, ObjectDeclaration, Old, @@ -310,7 +311,32 @@ def create_verify_procedure( [ ( Call("Composite_Field", [Variable("Fld")]), - [set_context_cursor_composite_field("Fld")], + # Componolit/RecordFlux#664 + # The provability of the context predicate is increased by duplicating + # the statement inside a case statement. Not required for versions newer + # than SPARK Community 2021. + [ + CaseStatement( + Variable("Fld"), + [ + *[ + ( + Variable(f.affixed_name), + [set_context_cursor_composite_field(f.affixed_name)], + ) + for f in composite_fields + ], + *( + [(Variable("others"), [NullStatement()])] + if scalar_fields + else [] + ), + ], + case_grouping=False, + ) + ] + if len(composite_fields) > 1 + else [set_context_cursor_composite_field("Fld")], ) ], [set_context_cursor_scalar()], diff --git a/tests/integration/messages/generated/rflx-universal-message.adb b/tests/integration/messages/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/messages/generated/rflx-universal-message.adb +++ b/tests/integration/messages/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/messages/generated/rflx-universal-message.ads +++ b/tests/integration/messages/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/messages/generated/rflx-universal-option.ads +++ b/tests/integration/messages/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.ads b/tests/integration/parameterized_messages/generated/rflx-test-message.ads index 947d22c5f..b53c940fa 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-message.ads @@ -271,7 +271,11 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Extension => + Field_Last'Result mod RFLX_Types.Byte'Size = 0); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_binding/generated/rflx-universal-message.adb b/tests/integration/session_binding/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_binding/generated/rflx-universal-message.adb +++ b/tests/integration/session_binding/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_binding/generated/rflx-universal-message.ads b/tests/integration/session_binding/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_binding/generated/rflx-universal-message.ads +++ b/tests/integration/session_binding/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_binding/generated/rflx-universal-option.ads b/tests/integration/session_binding/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_binding/generated/rflx-universal-option.ads +++ b/tests/integration/session_binding/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_channels/generated/rflx-universal-message.adb b/tests/integration/session_channels/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_channels/generated/rflx-universal-message.adb +++ b/tests/integration/session_channels/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_channels/generated/rflx-universal-message.ads b/tests/integration/session_channels/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_channels/generated/rflx-universal-message.ads +++ b/tests/integration/session_channels/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_channels/generated/rflx-universal-option.ads b/tests/integration/session_channels/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_channels/generated/rflx-universal-option.ads +++ b/tests/integration/session_channels/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.adb b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.adb +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.adb b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.adb +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_conversion/generated/rflx-universal-message.adb b/tests/integration/session_conversion/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-message.adb +++ b/tests/integration/session_conversion/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_conversion/generated/rflx-universal-message.ads b/tests/integration/session_conversion/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-message.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_conversion/generated/rflx-universal-option.ads b/tests/integration/session_conversion/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-option.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads b/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads index 2165e2f65..1412cdaa4 100644 --- a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads +++ b/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_functions/generated/rflx-universal-message.adb b/tests/integration/session_functions/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_functions/generated/rflx-universal-message.adb +++ b/tests/integration/session_functions/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_functions/generated/rflx-universal-message.ads b/tests/integration/session_functions/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_functions/generated/rflx-universal-message.ads +++ b/tests/integration/session_functions/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_functions/generated/rflx-universal-option.ads b/tests/integration/session_functions/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_functions/generated/rflx-universal-option.ads +++ b/tests/integration/session_functions/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_integration/generated/rflx-universal-message.adb b/tests/integration/session_integration/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_integration/generated/rflx-universal-message.adb +++ b/tests/integration/session_integration/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_integration/generated/rflx-universal-message.ads b/tests/integration/session_integration/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_integration/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_integration/generated/rflx-universal-option.ads b/tests/integration/session_integration/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_integration/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-message.adb b/tests/integration/session_integration_multiple/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-message.adb +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_minimal/generated/rflx-universal-message.adb b/tests/integration/session_minimal/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-message.adb +++ b/tests/integration/session_minimal/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_minimal/generated/rflx-universal-message.ads b/tests/integration/session_minimal/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-message.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_minimal/generated/rflx-universal-option.ads b/tests/integration/session_minimal/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-option.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.adb b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.adb +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads index 1475a620c..9b7bc2ca0 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads +++ b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Value => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_simple/generated/rflx-universal-message.adb b/tests/integration/session_simple/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_simple/generated/rflx-universal-message.adb +++ b/tests/integration/session_simple/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_simple/generated/rflx-universal-message.ads b/tests/integration/session_simple/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_simple/generated/rflx-universal-message.ads +++ b/tests/integration/session_simple/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_simple/generated/rflx-universal-option.ads b/tests/integration/session_simple/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_simple/generated/rflx-universal-option.ads +++ b/tests/integration/session_simple/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-message.adb b/tests/integration/session_variable_initialization/generated/rflx-universal-message.adb index 04a5f2b3b..912a39e44 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-message.adb +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-message.adb @@ -292,7 +292,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Data => + Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor); + when F_Option_Types => + Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor); + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Values => + Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads index 098ee194b..d7b4fb1e1 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads @@ -269,7 +269,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data | F_Option_Types | F_Options | F_Values => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads index 1f8e62d7a..b8f10c701 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index 563fab419..04f7e2899 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -266,7 +266,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Value => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index 7b58e89e7..dca9780a1 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -272,7 +272,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Payload => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index 937bfb387..c8b942ec1 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.ads @@ -266,7 +266,11 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Payload => + Field_Last'Result mod RFLX_Types.Byte'Size = 0); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 2165e2f65..1412cdaa4 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index 6c1270771..2597e8e83 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -290,7 +290,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index eb23f3afb..493fec70d 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -271,7 +271,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Option_Data => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-ipv4-packet.adb b/tests/spark/generated/rflx-ipv4-packet.adb index 236d87eeb..629ef55d6 100644 --- a/tests/spark/generated/rflx-ipv4-packet.adb +++ b/tests/spark/generated/rflx-ipv4-packet.adb @@ -348,7 +348,14 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Options => + Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor); + when F_Payload => + Ctx.Cursors (F_Payload) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Payload), Last => Field_Last (Ctx, F_Payload), Value => Value, Predecessor => Ctx.Cursors (F_Payload).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index b7dc3db1c..b9bbb4127 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -294,7 +294,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Options | F_Payload => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index 3f77e0070..c4a323fc4 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -262,7 +262,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Payload => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-sequence-message.adb b/tests/spark/generated/rflx-sequence-message.adb index aaeeb8f38..a78ac572a 100644 --- a/tests/spark/generated/rflx-sequence-message.adb +++ b/tests/spark/generated/rflx-sequence-message.adb @@ -231,7 +231,18 @@ is end case; pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); if Composite_Field (Fld) then - Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); + case Fld is + when F_Modular_Vector => + Ctx.Cursors (F_Modular_Vector) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Modular_Vector), Last => Field_Last (Ctx, F_Modular_Vector), Value => Value, Predecessor => Ctx.Cursors (F_Modular_Vector).Predecessor); + when F_Range_Vector => + Ctx.Cursors (F_Range_Vector) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Range_Vector), Last => Field_Last (Ctx, F_Range_Vector), Value => Value, Predecessor => Ctx.Cursors (F_Range_Vector).Predecessor); + when F_Enumeration_Vector => + Ctx.Cursors (F_Enumeration_Vector) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Enumeration_Vector), Last => Field_Last (Ctx, F_Enumeration_Vector), Value => Value, Predecessor => Ctx.Cursors (F_Enumeration_Vector).Predecessor); + when F_AV_Enumeration_Vector => + Ctx.Cursors (F_AV_Enumeration_Vector) := (State => S_Structural_Valid, First => Field_First (Ctx, F_AV_Enumeration_Vector), Last => Field_Last (Ctx, F_AV_Enumeration_Vector), Value => Value, Predecessor => Ctx.Cursors (F_AV_Enumeration_Vector).Predecessor); + when others => + null; + end case; else Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor); end if; diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index ed4a3e9aa..a7d6c457d 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -266,7 +266,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Modular_Vector | F_Range_Vector | F_Enumeration_Vector | F_AV_Enumeration_Vector => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index fd99e372d..c49cf8e2a 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -263,7 +263,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Messages => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; 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 63603530b..43295d051 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 @@ -263,7 +263,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Vector => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index 1475a620c..9b7bc2ca0 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/generated/rflx-tlv-message.ads @@ -264,7 +264,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Value => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index f0f4b675a..88257c3cc 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -268,7 +268,13 @@ is function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) - and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); + and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld), + Post => + (case Fld is + when F_Payload => + Field_Last'Result mod RFLX_Types.Byte'Size = 0, + when others => + True); function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;