diff --git a/examples/apps/ping/src/icmpv4.adb b/examples/apps/ping/src/icmpv4.adb index f463f0330d..ac5a8ea28e 100644 --- a/examples/apps/ping/src/icmpv4.adb +++ b/examples/apps/ping/src/icmpv4.adb @@ -57,6 +57,7 @@ is Success : Boolean; Ignore_Last : RFLX.RFLX_Builtin_Types.Index; Buffer : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(1 .. 1024 => 0); + Last : RFLX.RFLX_Builtin_Types.Index; begin Socket.Setup; if @@ -79,8 +80,8 @@ is pragma Loop_Invariant (Buffer /= null); pragma Loop_Invariant (Buffer'First = 1); pragma Loop_Invariant (Buffer'Length = 1024); - ICMPv4.Generate (Buffer, Address); - Socket.Send (Buffer.all (Buffer'First .. Buffer'First + 35), Address, Success); + Last := ICMPv4.Generate (Buffer, Address); + Socket.Send (Buffer.all (Buffer'First .. Last), Address, Success); if not Success then Ada.Text_IO.Put_Line ("Failed to send packet"); Free_Bytes_Ptr (Buffer); @@ -167,13 +168,13 @@ is -- Generate -- -------------- - procedure Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr; - Addr : RFLX.IPv4.Address) is + function Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr; + Addr : RFLX.IPv4.Address) return RFLX.RFLX_Builtin_Types.Index is use type RFLX.ICMP.Sequence_Number; use type RFLX.RFLX_Builtin_Types.Bit_Length; IP_Context : RFLX.IPv4.Packet.Context; ICMP_Context : RFLX.ICMP.Message.Context; - Data : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 8) := (others => 65); + Data : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 56) := (others => 65); function Valid_Length (L : RFLX.RFLX_Builtin_Types.Length) return Boolean is (L = Data'Length); procedure Process_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with @@ -183,7 +184,7 @@ is begin Buffer := Data; end Process_Data; - procedure Set_Data is new RFLX.ICMP.Message.Set_Bounded_Data (Process_Data, Valid_Length); + procedure Set_Data is new RFLX.ICMP.Message.Set_Data (Process_Data, Valid_Length); begin pragma Warnings (Off, "unused assignment to ""*_Context"""); RFLX.IPv4.Packet.Initialize (IP_Context, Buf); @@ -191,7 +192,7 @@ is RFLX.IPv4.Packet.Set_IHL (IP_Context, 5); RFLX.IPv4.Packet.Set_DSCP (IP_Context, 0); RFLX.IPv4.Packet.Set_ECN (IP_Context, 0); - RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 24); + RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 84); RFLX.IPv4.Packet.Set_Identification (IP_Context, 1); RFLX.IPv4.Packet.Set_Flag_R (IP_Context, False); RFLX.IPv4.Packet.Set_Flag_DF (IP_Context, False); @@ -214,13 +215,14 @@ is 0, 0, Sequence, Data)); RFLX.ICMP.Message.Set_Identifier (ICMP_Context, 0); RFLX.ICMP.Message.Set_Sequence_Number (ICMP_Context, Sequence); - Set_Data (ICMP_Context, 64); + Set_Data (ICMP_Context); RFLX.ICMP.Message.Take_Buffer (ICMP_Context, Buf); Sequence := Sequence + 1; else RFLX.IPv4.Packet.Take_Buffer (IP_Context, Buf); end if; pragma Warnings (On, "unused assignment to ""*_Context"""); + return RFLX.RFLX_Types.Byte_Index (RFLX.IPv4.Packet.Message_Last (IP_Context)); end Generate; ----------- diff --git a/examples/apps/ping/src/icmpv4.ads b/examples/apps/ping/src/icmpv4.ads index 54152f334b..9fc6948435 100644 --- a/examples/apps/ping/src/icmpv4.ads +++ b/examples/apps/ping/src/icmpv4.ads @@ -26,15 +26,14 @@ is SPARK.Heap.Dynamic_Memory), Input => Ada.Real_Time.Clock_Time); - procedure Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr; - Addr : RFLX.IPv4.Address) with + function Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr; + Addr : RFLX.IPv4.Address) return RFLX.RFLX_Builtin_Types.Index with Pre => Buf /= null and then Buf'Length = 1024 and then Buf'First = 1, Post => Buf /= null and then Buf'Length = Buf'Length'Old - and then Buf'First = Buf'First'Old, - Global => (In_Out => Ping_State); + and then Buf'First = Buf'First'Old; procedure Print (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr) with Pre => Buf /= null diff --git a/rflx/generator/common.py b/rflx/generator/common.py index baae25fd34..8bc3fa575e 100644 --- a/rflx/generator/common.py +++ b/rflx/generator/common.py @@ -459,6 +459,8 @@ def invalid_successors_invariant() -> ada.Expr: ] ), public_context_predicate(), + ada.LessEqual(ada.Variable("First"), ada.Variable("Message_Last")), + ada.LessEqual(ada.Variable("Message_Last"), ada.Variable("Last")), ada.ForAllIn( "F", ada.ValueRange(ada.First("Field"), ada.Last("Field")), @@ -480,7 +482,7 @@ def invalid_successors_invariant() -> ada.Expr: ada.Selected( ada.Indexed(ada.Variable("Cursors"), ada.Variable("F")), "Last" ), - ada.Variable("Last"), + ada.Variable("Message_Last"), ), ada.LessEqual( ada.Selected( @@ -576,17 +578,7 @@ def initialize_field_statements( "Reset_Dependent_Fields", [ada.Variable("Ctx"), ada.Variable(field.affixed_name)], ), - ada.Assignment( - "Ctx", - ada.Aggregate( - ada.Variable("Ctx.Buffer_First"), - ada.Variable("Ctx.Buffer_Last"), - ada.Variable("Ctx.First"), - ada.Variable("Last"), - ada.Variable("Ctx.Buffer"), - ada.Variable("Ctx.Cursors"), - ), - ), + ada.Assignment("Ctx.Message_Last", ada.Variable("Last")), # WORKAROUND: # Limitation of GNAT Community 2019 / SPARK Pro 20.0 # Provability of predicate is increased by adding part of diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py index 368a811fbe..35c36fb439 100644 --- a/rflx/generator/generator.py +++ b/rflx/generator/generator.py @@ -350,7 +350,7 @@ def __create_generic_message_unit(self, message: Message) -> None: unit += self.__create_initialized_function(message) unit += self.__create_take_buffer_procedure(context_invariant) unit += self.__create_has_buffer_function() - unit += self.__create_message_last_function(message) + unit += self.__create_message_last_function() unit += self.__create_path_condition_function(message) unit += self.__create_field_condition_function(message) unit += self.__create_field_size_function(message) @@ -538,6 +538,28 @@ def __create_cursor_type(message: Message) -> UnitPart: @staticmethod def __create_context_type() -> UnitPart: + """ + Components of a context type: + + Buffer_First, Buffer_Last: + The bounds of `Buffer` which are used to ensure that not a completely different + buffer is moved back into the context. + + First, Last: + The positions of the first and last usable bit of `Buffer`. These are hard bounds + which must not be changed during the lifetime of the context. + + Message_Last: + The position of the last bit of the message. The value is increased after each + parsed or set field. + + Buffer: + An access type refering to memory containing the binary message. + + Cursors: + An array of cursors representing the internal parser or serializer state. + """ + discriminants = [ Discriminant( ["Buffer_First", "Buffer_Last"], const.TYPES_INDEX, First(const.TYPES_INDEX) @@ -558,6 +580,7 @@ def __create_context_type() -> UnitPart: RecordType( "Context", [ + Component("Message_Last", const.TYPES_BIT_INDEX, Variable("First")), Component("Buffer", const.TYPES_BYTES_PTR, NULL), Component( "Cursors", @@ -587,6 +610,7 @@ def __create_context_type() -> UnitPart: Variable("Context.Buffer_Last"), Variable("Context.First"), Variable("Context.Last"), + Variable("Context.Message_Last"), Variable("Context.Buffer"), Variable("Context.Cursors"), ], @@ -660,6 +684,13 @@ def __create_initialize_procedure() -> UnitPart: [Variable("Ctx.Buffer_First")], ), ), + Equal( + Variable("Ctx.Last"), + Call( + const.TYPES * "Last_Bit_Index", + [Variable("Ctx.Buffer_Last")], + ), + ), Call("Initialized", [Variable("Ctx")]), ) ), @@ -754,6 +785,7 @@ def __create_restricted_initialize_procedure(message: Message) -> UnitPart: Variable("Buffer_Last"), Variable("First"), Variable("Last"), + Variable("First"), Variable("Buffer"), NamedAggregate( ( @@ -813,10 +845,7 @@ def __create_initialized_function(message: Message) -> UnitPart: ], ), Add( - Call( - const.TYPES * "Last_Bit_Index", - [Variable("Ctx.Buffer_Last")], - ), + Variable("Ctx.Last"), -Variable("Ctx.First"), Number(1), ), @@ -1548,62 +1577,14 @@ def __create_valid_predecessor_function( ) @staticmethod - def __create_message_last_function(message: Message) -> UnitPart: + def __create_message_last_function() -> UnitPart: specification = FunctionSpecification( "Message_Last", const.TYPES_BIT_INDEX, [Parameter(["Ctx"], "Context")] ) return UnitPart( - [ - SubprogramDeclaration( - specification, - [ - Precondition( - AndThen( - Call("Has_Buffer", [Variable("Ctx")]), - Call("Structural_Valid_Message", [Variable("Ctx")]), - ) - ) - ], - ) - ], - [ - ExpressionFunctionDeclaration( - specification, - If( - [ - ( - expr.AndThen( - expr.Call( - "Structural_Valid", - [ - expr.Indexed( - expr.Variable(expr.ID("Ctx") * "Cursors"), - expr.Variable( - l.source.affixed_name, immutable=True - ), - ) - ], - ), - l.condition, - ) - .substituted(common.substitution(message)) - .simplified() - .ada_expr(), - Selected( - Indexed( - Variable("Ctx.Cursors"), - Variable(l.source.affixed_name), - ), - "Last", - ), - ) - for l in message.incoming(FINAL) - ], - Variable(const.TYPES_UNREACHABLE_BIT_LENGTH), - ), - ) - ], + [SubprogramDeclaration(specification)], + [ExpressionFunctionDeclaration(specification, Variable("Ctx.Message_Last"))], ) @staticmethod @@ -1625,7 +1606,7 @@ def __create_available_space_function() -> UnitPart: ExpressionFunctionDeclaration( specification, Add( - Call(const.TYPES_LAST_BIT_INDEX, [Variable("Ctx.Buffer_Last")]), + Variable("Ctx.Last"), -Call("Field_First", [Variable("Ctx"), Variable("Fld")]), Number(1), ), @@ -2187,7 +2168,7 @@ def __create_valid_context_function( "Boolean", [ Parameter(["Buffer_First", "Buffer_Last"], const.TYPES_INDEX), - Parameter(["First", "Last"], const.TYPES_BIT_INDEX), + Parameter(["First", "Last", "Message_Last"], const.TYPES_BIT_INDEX), AccessParameter(["Buffer"], const.TYPES_BYTES, constant=True), Parameter(["Cursors"], "Field_Cursors"), ], diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py index 6a2ba00f04..60e120e37c 100644 --- a/rflx/generator/parser.py +++ b/rflx/generator/parser.py @@ -189,6 +189,9 @@ def create_verify_procedure( ) set_cursors_statements = [ + Assignment( + Variable("Ctx.Message_Last"), Call("Field_Last", [Variable("Ctx"), Variable("Fld")]) + ), IfStatement( [ ( diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py index ade002b245..b193ef0f67 100644 --- a/rflx/generator/serializer.py +++ b/rflx/generator/serializer.py @@ -35,7 +35,6 @@ Number, ObjectDeclaration, Old, - Or, OutParameter, Parameter, Postcondition, @@ -184,10 +183,7 @@ def create_internal_functions( ), GreaterEqual(Variable("Fst"), Variable("Ctx.First")), LessEqual(Variable("Fst"), Add(Variable("Lst"), Number(1))), - LessEqual( - Call(const.TYPES_BYTE_INDEX, [Variable("Lst")]), - Variable("Ctx.Buffer_Last"), - ), + LessEqual(Variable("Lst"), Variable("Ctx.Last")), ForAllIn( "F", Range("Field"), @@ -223,6 +219,7 @@ def create_internal_functions( Variable("Ctx.Buffer_First"), Variable("Ctx.Buffer_Last"), Variable("Ctx.First"), + Variable("Ctx.Last"), Variable("Ctx.Cursors"), ] ], @@ -351,17 +348,7 @@ def specification(field: Field, field_type: Type) -> ProcedureSpecification: Variable("Last"), ], ), - Assignment( - "Ctx", - Aggregate( - Variable("Ctx.Buffer_First"), - Variable("Ctx.Buffer_Last"), - Variable("Ctx.First"), - Variable("Last"), - Variable("Ctx.Buffer"), - Variable("Ctx.Cursors"), - ), - ), + Assignment(Variable("Ctx.Message_Last"), Variable("Last")), Assignment( Indexed(Variable("Ctx.Cursors"), Variable(f.affixed_name)), NamedAggregate( @@ -415,7 +402,7 @@ def specification(field: Field) -> ProcedureSpecification: Precondition( AndThen( *self.setter_preconditions(f), - *self.unbounded_composite_setter_preconditions(message, f), + *self.composite_setter_preconditions(message, f), Equal( Call( "Field_Size", @@ -463,17 +450,7 @@ def specification(field: Field) -> ProcedureSpecification: "Reset_Dependent_Fields", [Variable("Ctx"), Variable(f.affixed_name)], ), - Assignment( - "Ctx", - Aggregate( - Variable("Ctx.Buffer_First"), - Variable("Ctx.Buffer_Last"), - Variable("Ctx.First"), - Variable("Last"), - Variable("Ctx.Buffer"), - Variable("Ctx.Cursors"), - ), - ), + Assignment(Variable("Ctx.Message_Last"), Variable("Last")), Assignment( Indexed(Variable("Ctx.Cursors"), Variable(f.affixed_name)), NamedAggregate( @@ -520,12 +497,6 @@ def create_composite_setter_procedures(self, message: Message) -> UnitPart: def specification(field: Field) -> ProcedureSpecification: return ProcedureSpecification(f"Set_{field.name}", [InOutParameter(["Ctx"], "Context")]) - def specification_bounded(field: Field) -> ProcedureSpecification: - return ProcedureSpecification( - f"Set_Bounded_{field.name}", - [InOutParameter(["Ctx"], "Context"), Parameter(["Size"], const.TYPES_BIT_LENGTH)], - ) - def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]: return [ FormalSubprogramDeclaration( @@ -551,7 +522,7 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]: Precondition( AndThen( *self.setter_preconditions(f), - *self.unbounded_composite_setter_preconditions(message, f), + *self.composite_setter_preconditions(message, f), Call( "Valid_Length", [ @@ -583,37 +554,7 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]: formal_parameters(f), ) for f, t in message.types.items() - if isinstance(t, Opaque) and unbounded_setter_required(message, f) - ] - + [ - SubprogramDeclaration( - specification_bounded(f), - [ - Precondition( - AndThen( - *self.setter_preconditions(f), - *self.bounded_composite_setter_preconditions(message, f), - Call( - "Valid_Length", - [ - Call( - const.TYPES_LENGTH, - [Div(Variable("Size"), Size(const.TYPES_BYTE))], - ) - ], - ), - ) - ), - Postcondition( - And( - *self.composite_setter_postconditions(message, f), - ) - ), - ], - formal_parameters(f), - ) - for f, t in message.types.items() - if isinstance(t, Opaque) and bounded_setter_required(message, f) + if isinstance(t, Opaque) and setter_required(message, f) ], [ SubprogramBody( @@ -644,54 +585,7 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]: ], ) for f, t in message.types.items() - if isinstance(t, Opaque) and unbounded_setter_required(message, f) - ] - + [ - SubprogramBody( - specification_bounded(f), - [ - ObjectDeclaration( - ["First"], - const.TYPES_BIT_INDEX, - Call( - "Field_First", - [Variable("Ctx"), Variable(f.affixed_name)], - ), - True, - ), - ObjectDeclaration( - ["Last"], - const.TYPES_BIT_INDEX, - Add(Variable("First"), Variable("Size"), -Number(1)), - True, - ), - ExpressionFunctionDeclaration( - FunctionSpecification("Buffer_First", const.TYPES_INDEX), - Call(const.TYPES_BYTE_INDEX, [Variable("First")]), - ), - ExpressionFunctionDeclaration( - FunctionSpecification("Buffer_Last", const.TYPES_INDEX), - Call(const.TYPES_BYTE_INDEX, [Variable("Last")]), - ), - ], - [ - CallStatement( - f"Initialize_Bounded_{f.name}", [Variable("Ctx"), Variable("Size")] - ), - CallStatement( - f"Process_{f.name}", - [ - Slice( - Selected(Variable("Ctx.Buffer"), "all"), - Variable("Buffer_First"), - Variable("Buffer_Last"), - ), - ], - ), - ], - ) - for f, t in message.types.items() - if isinstance(t, Opaque) and bounded_setter_required(message, f) + if isinstance(t, Opaque) and setter_required(message, f) ], ) @@ -701,12 +595,6 @@ def specification(field: Field) -> ProcedureSpecification: f"Initialize_{field.name}", [InOutParameter(["Ctx"], "Context")] ) - def specification_bounded(field: Field) -> ProcedureSpecification: - return ProcedureSpecification( - f"Initialize_Bounded_{field.name}", - [InOutParameter(["Ctx"], "Context"), Parameter(["Size"], const.TYPES_BIT_LENGTH)], - ) - return UnitPart( [ SubprogramDeclaration( @@ -715,7 +603,7 @@ def specification_bounded(field: Field) -> ProcedureSpecification: Precondition( AndThen( *self.setter_preconditions(f), - *self.unbounded_composite_setter_preconditions(message, f), + *self.composite_setter_preconditions(message, f), ) ), Postcondition( @@ -726,23 +614,7 @@ def specification_bounded(field: Field) -> ProcedureSpecification: ], ) for f, t in message.types.items() - if isinstance(t, Opaque) and unbounded_setter_required(message, f) - ] - + [ - SubprogramDeclaration( - specification_bounded(f), - [ - Precondition( - AndThen( - *self.setter_preconditions(f), - *self.bounded_composite_setter_preconditions(message, f), - ) - ), - Postcondition(And(*self.composite_setter_postconditions(message, f))), - ], - ) - for f, t in message.types.items() - if isinstance(t, Opaque) and bounded_setter_required(message, f) + if isinstance(t, Opaque) and setter_required(message, f) ], [ SubprogramBody( @@ -751,32 +623,7 @@ def specification_bounded(field: Field) -> ProcedureSpecification: common.initialize_field_statements(message, f, self.prefix), ) for f, t in message.types.items() - if isinstance(t, Opaque) and unbounded_setter_required(message, f) - ] - + [ - SubprogramBody( - specification_bounded(f), - [ - ObjectDeclaration( - ["First"], - const.TYPES_BIT_INDEX, - Call( - "Field_First", - [Variable("Ctx"), Variable(f.affixed_name)], - ), - True, - ), - ObjectDeclaration( - ["Last"], - const.TYPES_BIT_INDEX, - Add(Variable("First"), Variable("Size"), -Number(1)), - True, - ), - ], - common.initialize_field_statements(message, f, self.prefix), - ) - for f, t in message.types.items() - if isinstance(t, Opaque) and bounded_setter_required(message, f) + if isinstance(t, Opaque) and setter_required(message, f) ], ) @@ -807,6 +654,7 @@ def setter_postconditions(message: Message, field: Field) -> Sequence[Expr]: Variable("Ctx.Buffer_First"), Variable("Ctx.Buffer_Last"), Variable("Ctx.First"), + Variable("Ctx.Last"), Call( "Predecessor", [Variable("Ctx"), Variable(field.affixed_name)], @@ -832,7 +680,7 @@ def composite_setter_postconditions(self, message: Message, field: Field) -> Seq ] @staticmethod - def unbounded_composite_setter_preconditions(message: Message, field: Field) -> Sequence[Expr]: + def composite_setter_preconditions(message: Message, field: Field) -> Sequence[Expr]: return [ Call( "Field_Condition", @@ -874,87 +722,10 @@ def unbounded_composite_setter_preconditions(message: Message, field: Field) -> ), ] - @staticmethod - def bounded_composite_setter_preconditions(message: Message, field: Field) -> Sequence[Expr]: - return [ - Call( - "Field_Condition", - [ - Variable("Ctx"), - NamedAggregate(("Fld", Variable(field.affixed_name))), - ] - + ([Variable("Size")] if common.size_dependent_condition(message) else []), - ), - GreaterEqual( - Call( - "Available_Space", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Variable("Size"), - ), - LessEqual( - Add( - Call( - "Field_First", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Variable("Size"), - ), - Div(Last(const.TYPES_BIT_INDEX), Number(2)), - ), - Or( - *[ - And( - *[ - Call( - "Valid", - [Variable("Ctx"), Variable(field.affixed_name)], - ) - for field in message.fields - if expr.Variable(field.name) in l.condition.variables() - ], - l.condition.substituted( - mapping={ - expr.Variable(field.name): expr.Call( - f"Get_{field.name}", [expr.Variable("Ctx")] - ) - for field in message.fields - if expr.Variable(field.name) in l.condition.variables() - } - ).ada_expr(), - ) - for l in message.incoming(field) - if expr.Last("Message") in l.size - ] - ), - Equal( - Mod( - Call( - "Field_First", - [Variable("Ctx"), Variable(field.affixed_name)], - ), - Size(const.TYPES_BYTE), - ), - Number(1), - ), - Equal( - Mod(Variable("Size"), Size(const.TYPES_BYTE)), - Number(0), - ), - ] - -def unbounded_setter_required(message: Message, field: Field) -> bool: +def setter_required(message: Message, field: Field) -> bool: return any( True for l in message.incoming(field) if expr.Size("Message") not in l.size and expr.Last("Message") not in l.size ) - - -def bounded_setter_required(message: Message, field: Field) -> bool: - return any( - True - for l in message.incoming(field) - if expr.Size("Message") in l.size or expr.Last("Message") in l.size - ) diff --git a/tests/data/models.py b/tests/data/models.py index a50e17b27c..bd408f895e 100644 --- a/tests/data/models.py +++ b/tests/data/models.py @@ -196,6 +196,19 @@ {Field("Length"): ARRAYS_LENGTH, Field("Messages"): ARRAYS_INNER_MESSAGES}, skip_proof=True, ) +ARRAYS_ARRAY_SIZE_DEFINED_BY_MESSAGE_SIZE = Message( + "Arrays::Array_Size_Defined_By_Message_Size", + [ + Link(INITIAL, Field("Header")), + Link(Field("Header"), Field("Vector"), size=Sub(Size("Message"), Size("Header"))), + Link(Field("Vector"), FINAL), + ], + { + Field("Header"): ARRAYS_ENUMERATION, + Field("Vector"): ARRAYS_MODULAR_VECTOR, + }, + skip_proof=True, +) ARRAYS_MODEL = Model( [ ARRAYS_LENGTH, @@ -211,6 +224,7 @@ ARRAYS_INNER_MESSAGE, ARRAYS_INNER_MESSAGES, ARRAYS_MESSAGES_MESSAGE, + ARRAYS_ARRAY_SIZE_DEFINED_BY_MESSAGE_SIZE, ] ) diff --git a/tests/spark/generated/rflx-arrays-array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-array_size_defined_by_message_size.ads new file mode 100644 index 0000000000..e107cfb53e --- /dev/null +++ b/tests/spark/generated/rflx-arrays-array_size_defined_by_message_size.ads @@ -0,0 +1,7 @@ +pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); +pragma SPARK_Mode; +with RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size; +with RFLX.RFLX_Types; +with RFLX.Arrays.Modular_Vector; + +package RFLX.Arrays.Array_Size_Defined_By_Message_Size is new RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size (RFLX.RFLX_Types, RFLX.Arrays.Modular_Vector); diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb new file mode 100644 index 0000000000..72d660972b --- /dev/null +++ b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb @@ -0,0 +1,444 @@ +pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); + +package body RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size with + SPARK_Mode +is + + procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr) is + begin + Initialize (Ctx, Buffer, Types.First_Bit_Index (Buffer'First), Types.Last_Bit_Index (Buffer'Last)); + end Initialize; + + procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr; First, Last : Types.Bit_Index) is + Buffer_First : constant Types.Index := Buffer'First; + Buffer_Last : constant Types.Index := Buffer'Last; + begin + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Header => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Buffer := null; + end Initialize; + + function Initialized (Ctx : Context) return Boolean is + (Valid_Next (Ctx, F_Header) + and then Available_Space (Ctx, F_Header) = Ctx.Last - Ctx.First + 1 + and then Invalid (Ctx, F_Header) + and then Invalid (Ctx, F_Vector)); + + procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr) is + begin + Buffer := Ctx.Buffer; + Ctx.Buffer := null; + end Take_Buffer; + + function Has_Buffer (Ctx : Context) return Boolean is + (Ctx.Buffer /= null); + + function Message_Last (Ctx : Context) return Types.Bit_Index is + (Ctx.Message_Last); + + function Path_Condition (Ctx : Context; Fld : Field) return Boolean is + ((case Ctx.Cursors (Fld).Predecessor is + when F_Initial => + (case Fld is + when F_Header => + True, + when others => + False), + when F_Header => + (case Fld is + when F_Vector => + True, + when others => + False), + when F_Vector | F_Final => + False)); + + function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean is + ((case Val.Fld is + when F_Initial | F_Header | F_Vector => + True, + when F_Final => + False)); + + function Field_Size (Ctx : Context; Fld : Field) return Types.Bit_Length is + ((case Ctx.Cursors (Fld).Predecessor is + when F_Initial => + (case Fld is + when F_Header => + RFLX.Arrays.Enumeration_Base'Size, + when others => + Types.Unreachable_Bit_Length), + when F_Header => + (case Fld is + when F_Vector => + Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1), + when others => + Types.Unreachable_Bit_Length), + when F_Vector | F_Final => + 0)); + + function Field_First (Ctx : Context; Fld : Field) return Types.Bit_Index is + ((case Fld is + when F_Header => + Ctx.First, + when F_Vector => + (if + Ctx.Cursors (Fld).Predecessor = F_Header + then + Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1 + else + Types.Unreachable_Bit_Length))); + + function Field_Last (Ctx : Context; Fld : Field) return Types.Bit_Index is + (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is + ((case Fld is + when F_Initial => + F_Initial, + when others => + Ctx.Cursors (Fld).Predecessor)); + + function Successor (Ctx : Context; Fld : Field) return Virtual_Field is + ((case Fld is + when F_Header => + F_Vector, + when F_Vector => + F_Final)) + with + Pre => + Has_Buffer (Ctx) + and Structural_Valid (Ctx, Fld) + and Valid_Predecessor (Ctx, Fld); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is + ((case Fld is + when F_Initial => + True, + when F_Header => + Ctx.Cursors (Fld).Predecessor = F_Initial, + when F_Vector => + (Valid (Ctx.Cursors (F_Header)) + and Ctx.Cursors (Fld).Predecessor = F_Header), + when F_Final => + (Structural_Valid (Ctx.Cursors (F_Vector)) + and Ctx.Cursors (Fld).Predecessor = F_Vector))); + + function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is + ((case Fld is + when F_Header => + Invalid (Ctx.Cursors (F_Vector)), + when F_Vector => + True)); + + function Valid_Next (Ctx : Context; Fld : Field) return Boolean is + (Valid_Predecessor (Ctx, Fld) + and then Path_Condition (Ctx, Fld)); + + function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is + (Ctx.Last - Field_First (Ctx, Fld) + 1); + + function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Buffer /= null + and Ctx.First <= Types.Bit_Index'Last / 2 + and Field_First (Ctx, Fld) <= Types.Bit_Index'Last / 2 + and Field_Size (Ctx, Fld) >= 0 + and Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2 + and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2 + and Ctx.First <= Field_First (Ctx, Fld) + and Ctx.Last >= Field_Last (Ctx, Fld)) + with + Pre => + Has_Buffer (Ctx) + and Valid_Next (Ctx, Fld); + + function Equal (Ctx : Context; Fld : Field; Data : Types.Bytes) return Boolean is + (Sufficient_Buffer_Length (Ctx, Fld) + and then (case Fld is + when F_Vector => + Ctx.Buffer.all (Types.Byte_Index (Field_First (Ctx, Fld)) .. Types.Byte_Index (Field_Last (Ctx, Fld))) = Data, + when others => + False)); + + procedure Reset_Dependent_Fields (Ctx : in out Context; Fld : Field) with + Pre => + Valid_Next (Ctx, Fld), + Post => + Valid_Next (Ctx, Fld) + and Invalid (Ctx.Cursors (Fld)) + and Invalid_Successor (Ctx, Fld) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Ctx.Cursors (Fld).Predecessor = Ctx.Cursors (Fld).Predecessor'Old + and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old + and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old + and (case Fld is + when F_Header => + Invalid (Ctx, F_Header) + and Invalid (Ctx, F_Vector), + when F_Vector => + Ctx.Cursors (F_Header) = Ctx.Cursors (F_Header)'Old + and Invalid (Ctx, F_Vector)) + is + First : constant Types.Bit_Length := Field_First (Ctx, Fld) with + Ghost; + Size : constant Types.Bit_Length := Field_Size (Ctx, Fld) with + Ghost; + begin + pragma Assert (Field_First (Ctx, Fld) = First + and Field_Size (Ctx, Fld) = Size); + case Fld is + when F_Header => + Ctx.Cursors (F_Vector) := (S_Invalid, F_Final); + Ctx.Cursors (F_Header) := (S_Invalid, Ctx.Cursors (F_Header).Predecessor); + pragma Assert (Field_First (Ctx, Fld) = First + and Field_Size (Ctx, Fld) = Size); + when F_Vector => + Ctx.Cursors (F_Vector) := (S_Invalid, Ctx.Cursors (F_Vector).Predecessor); + pragma Assert (Field_First (Ctx, Fld) = First + and Field_Size (Ctx, Fld) = Size); + end case; + end Reset_Dependent_Fields; + + function Composite_Field (Fld : Field) return Boolean is + ((case Fld is + when F_Header => + False, + when F_Vector => + True)); + + function Get_Field_Value (Ctx : Context; Fld : Field) return Field_Dependent_Value with + Pre => + Has_Buffer (Ctx) + and then Valid_Next (Ctx, Fld) + and then Sufficient_Buffer_Length (Ctx, Fld), + Post => + Get_Field_Value'Result.Fld = Fld + is + First : constant Types.Bit_Index := Field_First (Ctx, Fld); + Last : constant Types.Bit_Index := Field_Last (Ctx, Fld); + function Buffer_First return Types.Index is + (Types.Byte_Index (First)); + function Buffer_Last return Types.Index is + (Types.Byte_Index (Last)); + function Offset return Types.Offset is + (Types.Offset ((8 - Last mod 8) mod 8)); + function Extract is new Types.Extract (RFLX.Arrays.Enumeration_Base); + begin + return ((case Fld is + when F_Header => + (Fld => F_Header, Header_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)), + when F_Vector => + (Fld => F_Vector))); + end Get_Field_Value; + + procedure Verify (Ctx : in out Context; Fld : Field) is + Value : Field_Dependent_Value; + begin + if + Has_Buffer (Ctx) + and then Invalid (Ctx.Cursors (Fld)) + and then Valid_Predecessor (Ctx, Fld) + and then Path_Condition (Ctx, Fld) + then + if Sufficient_Buffer_Length (Ctx, Fld) then + Value := Get_Field_Value (Ctx, Fld); + if + Valid_Value (Value) + and Field_Condition (Ctx, Value) + then + Ctx.Message_Last := Field_Last (Ctx, Fld); + 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); + 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; + pragma Assert ((if + Structural_Valid (Ctx.Cursors (F_Header)) + then + Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1 = RFLX.Arrays.Enumeration_Base'Size + and then Ctx.Cursors (F_Header).Predecessor = F_Initial + and then Ctx.Cursors (F_Header).First = Ctx.First + and then (if + Structural_Valid (Ctx.Cursors (F_Vector)) + then + Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1) + and then Ctx.Cursors (F_Vector).Predecessor = F_Header + and then Ctx.Cursors (F_Vector).First = Ctx.Cursors (F_Header).Last + 1))); + if Fld = F_Header then + Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld); + elsif Fld = F_Vector then + Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld); + end if; + else + Ctx.Cursors (Fld) := (State => S_Invalid, Predecessor => F_Final); + end if; + else + Ctx.Cursors (Fld) := (State => S_Incomplete, Predecessor => F_Final); + end if; + end if; + end Verify; + + procedure Verify_Message (Ctx : in out Context) is + begin + Verify (Ctx, F_Header); + Verify (Ctx, F_Vector); + end Verify_Message; + + function Present (Ctx : Context; Fld : Field) return Boolean is + (Structural_Valid (Ctx.Cursors (Fld)) + and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1); + + function Structural_Valid (Ctx : Context; Fld : Field) return Boolean is + ((Ctx.Cursors (Fld).State = S_Valid + or Ctx.Cursors (Fld).State = S_Structural_Valid)); + + function Valid (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Valid + and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1); + + function Incomplete (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Incomplete); + + function Invalid (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Invalid + or Ctx.Cursors (Fld).State = S_Incomplete); + + function Structural_Valid_Message (Ctx : Context) return Boolean is + (Valid (Ctx, F_Header) + and then Structural_Valid (Ctx, F_Vector)); + + function Valid_Message (Ctx : Context) return Boolean is + (Valid (Ctx, F_Header) + and then Valid (Ctx, F_Vector)); + + function Incomplete_Message (Ctx : Context) return Boolean is + (Incomplete (Ctx, F_Header) + or Incomplete (Ctx, F_Vector)); + + function Get_Header (Ctx : Context) return RFLX.Arrays.Enumeration is + (To_Actual (Ctx.Cursors (F_Header).Value.Header_Value)); + + procedure Get_Vector (Ctx : Context) is + First : constant Types.Index := Types.Byte_Index (Ctx.Cursors (F_Vector).First); + Last : constant Types.Index := Types.Byte_Index (Ctx.Cursors (F_Vector).Last); + begin + Process_Vector (Ctx.Buffer.all (First .. Last)); + end Get_Vector; + + procedure Set_Field_Value (Ctx : in out Context; Val : Field_Dependent_Value; Fst, Lst : out Types.Bit_Index) with + Pre => + not Ctx'Constrained + and then Has_Buffer (Ctx) + and then Val.Fld in Field'Range + and then Valid_Next (Ctx, Val.Fld) + and then Available_Space (Ctx, Val.Fld) >= Field_Size (Ctx, Val.Fld) + and then (for all F in Field'Range => + (if + Structural_Valid (Ctx.Cursors (F)) + then + Ctx.Cursors (F).Last <= Field_Last (Ctx, Val.Fld))), + Post => + Has_Buffer (Ctx) + and Fst = Field_First (Ctx, Val.Fld) + and Lst = Field_Last (Ctx, Val.Fld) + and Fst >= Ctx.First + and Fst <= Lst + 1 + and Lst <= Ctx.Last + and (for all F in Field'Range => + (if + Structural_Valid (Ctx.Cursors (F)) + then + Ctx.Cursors (F).Last <= Lst)) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Ctx.Cursors = Ctx.Cursors'Old + is + First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); + Last : constant Types.Bit_Index := Field_Last (Ctx, Val.Fld); + function Buffer_First return Types.Index is + (Types.Byte_Index (First)); + function Buffer_Last return Types.Index is + (Types.Byte_Index (Last)); + function Offset return Types.Offset is + (Types.Offset ((8 - Last mod 8) mod 8)); + procedure Insert is new Types.Insert (RFLX.Arrays.Enumeration_Base); + begin + Fst := First; + Lst := Last; + case Val.Fld is + when F_Initial => + null; + when F_Header => + Insert (Val.Header_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset); + when F_Vector | F_Final => + null; + end case; + end Set_Field_Value; + + procedure Set_Header (Ctx : in out Context; Val : RFLX.Arrays.Enumeration) is + Field_Value : constant Field_Dependent_Value := (F_Header, To_Base (Val)); + First, Last : Types.Bit_Index; + begin + Reset_Dependent_Fields (Ctx, F_Header); + Set_Field_Value (Ctx, Field_Value, First, Last); + Ctx.Message_Last := Last; + Ctx.Cursors (F_Header) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Header).Predecessor); + Ctx.Cursors (Successor (Ctx, F_Header)) := (State => S_Invalid, Predecessor => F_Header); + end Set_Header; + + procedure Set_Vector_Empty (Ctx : in out Context) is + First : constant Types.Bit_Index := Field_First (Ctx, F_Vector); + Last : constant Types.Bit_Index := Field_Last (Ctx, F_Vector); + begin + Reset_Dependent_Fields (Ctx, F_Vector); + Ctx.Message_Last := Last; + Ctx.Cursors (F_Vector) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Vector), Predecessor => Ctx.Cursors (F_Vector).Predecessor); + Ctx.Cursors (Successor (Ctx, F_Vector)) := (State => S_Invalid, Predecessor => F_Vector); + end Set_Vector_Empty; + + procedure Switch_To_Vector (Ctx : in out Context; Seq_Ctx : out Modular_Vector_Sequence.Context) is + First : constant Types.Bit_Index := Field_First (Ctx, F_Vector); + Last : constant Types.Bit_Index := Field_Last (Ctx, F_Vector); + Buffer : Types.Bytes_Ptr; + begin + if Invalid (Ctx, F_Vector) then + Reset_Dependent_Fields (Ctx, F_Vector); + Ctx.Message_Last := Last; + pragma Assert ((if + Structural_Valid (Ctx.Cursors (F_Header)) + then + Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1 = RFLX.Arrays.Enumeration_Base'Size + and then Ctx.Cursors (F_Header).Predecessor = F_Initial + and then Ctx.Cursors (F_Header).First = Ctx.First + and then (if + Structural_Valid (Ctx.Cursors (F_Vector)) + then + Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1) + and then Ctx.Cursors (F_Vector).Predecessor = F_Header + and then Ctx.Cursors (F_Vector).First = Ctx.Cursors (F_Header).Last + 1))); + Ctx.Cursors (F_Vector) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Vector), Predecessor => Ctx.Cursors (F_Vector).Predecessor); + Ctx.Cursors (Successor (Ctx, F_Vector)) := (State => S_Invalid, Predecessor => F_Vector); + end if; + Take_Buffer (Ctx, Buffer); + pragma Warnings (Off, "unused assignment to ""Buffer"""); + Modular_Vector_Sequence.Initialize (Seq_Ctx, Buffer, Ctx.Buffer_First, Ctx.Buffer_Last, First, Last); + pragma Warnings (On, "unused assignment to ""Buffer"""); + end Switch_To_Vector; + + procedure Update_Vector (Ctx : in out Context; Seq_Ctx : in out Modular_Vector_Sequence.Context) is + Valid_Sequence : constant Boolean := Modular_Vector_Sequence.Valid (Seq_Ctx); + Buffer : Types.Bytes_Ptr; + begin + Modular_Vector_Sequence.Take_Buffer (Seq_Ctx, Buffer); + Ctx.Buffer := Buffer; + if Valid_Sequence then + Ctx.Cursors (F_Vector) := (State => S_Valid, First => Ctx.Cursors (F_Vector).First, Last => Ctx.Cursors (F_Vector).Last, Value => Ctx.Cursors (F_Vector).Value, Predecessor => Ctx.Cursors (F_Vector).Predecessor); + end if; + end Update_Vector; + +end RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size; diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads new file mode 100644 index 0000000000..8d6bad7520 --- /dev/null +++ b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads @@ -0,0 +1,412 @@ +pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); +with RFLX.RFLX_Generic_Types; +with RFLX.RFLX_Scalar_Sequence; + +generic + with package Types is new RFLX.RFLX_Generic_Types (<>); + with package Modular_Vector_Sequence is new RFLX.RFLX_Scalar_Sequence (Types, others => <>); +package RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size with + SPARK_Mode, + Annotate => + (GNATprove, Terminating) +is + + pragma Warnings (Off, "use clause for type ""U64"" * has no effect"); + + use type Types.Bytes, Types.Bytes_Ptr, Types.Index, Types.Bit_Index, Types.U64; + + pragma Warnings (On, "use clause for type ""U64"" * has no effect"); + + type Virtual_Field is (F_Initial, F_Header, F_Vector, F_Final); + + subtype Field is Virtual_Field range F_Header .. F_Vector; + + type Field_Cursor is private with + Default_Initial_Condition => + False; + + type Field_Cursors is private with + Default_Initial_Condition => + False; + + type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is private with + Default_Initial_Condition => + Types.Byte_Index (First) >= Buffer_First + and Types.Byte_Index (Last) <= Buffer_Last + and First <= Last + and Last <= Types.Bit_Index'Last / 2; + + type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is + record + case Fld is + when F_Initial | F_Vector | F_Final => + null; + when F_Header => + Header_Value : RFLX.Arrays.Enumeration_Base; + end case; + end record; + + procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr) with + Pre => + not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last <= Types.Index'Last / 2, + Post => + Has_Buffer (Ctx) + and Buffer = null + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) + and Initialized (Ctx), + Depends => + (Ctx => Buffer, Buffer => null); + + procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr; First, Last : Types.Bit_Index) with + Pre => + not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Types.Byte_Index (First) >= Buffer'First + and then Types.Byte_Index (Last) <= Buffer'Last + and then First <= Last + and then Last <= Types.Bit_Index'Last / 2, + Post => + Buffer = null + and Has_Buffer (Ctx) + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = First + and Ctx.Last = Last + and Initialized (Ctx), + Depends => + (Ctx => (Buffer, First, Last), Buffer => null); + + function Initialized (Ctx : Context) return Boolean with + Ghost; + + procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr) with + Pre => + Has_Buffer (Ctx), + Post => + not Has_Buffer (Ctx) + and Buffer /= null + and Ctx.Buffer_First = Buffer'First + and Ctx.Buffer_Last = Buffer'Last + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Context_Cursors (Ctx) = Context_Cursors (Ctx)'Old, + Depends => + (Ctx => Ctx, Buffer => Ctx); + + function Has_Buffer (Ctx : Context) return Boolean; + + function Message_Last (Ctx : Context) return Types.Bit_Index; + + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with + Pre => + Valid_Predecessor (Ctx, Fld); + + function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with + Pre => + Has_Buffer (Ctx) + and Val.Fld in Field'Range + and Valid_Predecessor (Ctx, Val.Fld); + + function Field_Size (Ctx : Context; Fld : Field) return Types.Bit_Length with + Pre => + Valid_Next (Ctx, Fld); + + function Field_First (Ctx : Context; Fld : Field) return Types.Bit_Index with + Pre => + Valid_Next (Ctx, Fld); + + function Field_Last (Ctx : Context; Fld : Field) return Types.Bit_Index with + Pre => + Valid_Next (Ctx, Fld); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + + function Valid_Next (Ctx : Context; Fld : Field) return Boolean; + + function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length with + Pre => + Valid_Next (Ctx, Fld); + + function Equal (Ctx : Context; Fld : Field; Data : Types.Bytes) return Boolean with + Pre => + Has_Buffer (Ctx) + and Valid_Next (Ctx, Fld); + + procedure Verify (Ctx : in out Context; Fld : Field) with + Post => + Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old; + + procedure Verify_Message (Ctx : in out Context) with + Post => + Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old; + + function Present (Ctx : Context; Fld : Field) return Boolean; + + function Structural_Valid (Ctx : Context; Fld : Field) return Boolean; + + function Valid (Ctx : Context; Fld : Field) return Boolean with + Post => + (if + Valid'Result + then + Structural_Valid (Ctx, Fld) + and Present (Ctx, Fld)); + + function Incomplete (Ctx : Context; Fld : Field) return Boolean; + + function Invalid (Ctx : Context; Fld : Field) return Boolean; + + function Structural_Valid_Message (Ctx : Context) return Boolean with + Pre => + Has_Buffer (Ctx); + + function Valid_Message (Ctx : Context) return Boolean with + Pre => + Has_Buffer (Ctx); + + function Incomplete_Message (Ctx : Context) return Boolean; + + function Get_Header (Ctx : Context) return RFLX.Arrays.Enumeration with + Pre => + Valid (Ctx, F_Header); + + generic + with procedure Process_Vector (Vector : Types.Bytes); + procedure Get_Vector (Ctx : Context) with + Pre => + Has_Buffer (Ctx) + and Present (Ctx, F_Vector); + + procedure Set_Header (Ctx : in out Context; Val : RFLX.Arrays.Enumeration) with + Pre => + not Ctx'Constrained + and then Has_Buffer (Ctx) + and then Valid_Next (Ctx, F_Header) + and then Field_Last (Ctx, F_Header) <= Types.Bit_Index'Last / 2 + and then Field_Condition (Ctx, (F_Header, To_Base (Val))) + and then True + and then Available_Space (Ctx, F_Header) >= Field_Size (Ctx, F_Header), + Post => + Has_Buffer (Ctx) + and Valid (Ctx, F_Header) + and Get_Header (Ctx) = Val + and Invalid (Ctx, F_Vector) + and (Predecessor (Ctx, F_Vector) = F_Header + and Valid_Next (Ctx, F_Vector)) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Predecessor (Ctx, F_Header) = Predecessor (Ctx, F_Header)'Old + and Valid_Next (Ctx, F_Header) = Valid_Next (Ctx, F_Header)'Old; + + procedure Set_Vector_Empty (Ctx : in out Context) with + Pre => + not Ctx'Constrained + and then Has_Buffer (Ctx) + and then Valid_Next (Ctx, F_Vector) + and then Field_Last (Ctx, F_Vector) <= Types.Bit_Index'Last / 2 + and then Field_Condition (Ctx, (Fld => F_Vector)) + and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector) + and then Field_First (Ctx, F_Vector) mod Types.Byte'Size = 1 + and then Field_Size (Ctx, F_Vector) mod Types.Byte'Size = 0 + and then Field_Size (Ctx, F_Vector) = 0, + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Predecessor (Ctx, F_Vector) = Predecessor (Ctx, F_Vector)'Old + and Valid_Next (Ctx, F_Vector) = Valid_Next (Ctx, F_Vector)'Old + and Get_Header (Ctx) = Get_Header (Ctx)'Old + and Structural_Valid (Ctx, F_Vector); + + procedure Switch_To_Vector (Ctx : in out Context; Seq_Ctx : out Modular_Vector_Sequence.Context) with + Pre => + not Ctx'Constrained + and then not Seq_Ctx'Constrained + and then Has_Buffer (Ctx) + and then Valid_Next (Ctx, F_Vector) + and then Field_Size (Ctx, F_Vector) > 0 + and then Field_Last (Ctx, F_Vector) <= Types.Bit_Index'Last / 2 + and then Field_Condition (Ctx, (Fld => F_Vector)) + and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector), + Post => + not Has_Buffer (Ctx) + and Modular_Vector_Sequence.Has_Buffer (Seq_Ctx) + and Ctx.Buffer_First = Seq_Ctx.Buffer_First + and Ctx.Buffer_Last = Seq_Ctx.Buffer_Last + and Seq_Ctx.First = Field_First (Ctx, F_Vector) + and Seq_Ctx.Last = Field_Last (Ctx, F_Vector) + and Modular_Vector_Sequence.Index (Seq_Ctx) = Seq_Ctx.First + and Present (Ctx, F_Vector) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Predecessor (Ctx, F_Vector) = Predecessor (Ctx, F_Vector)'Old + and Path_Condition (Ctx, F_Vector) = Path_Condition (Ctx, F_Vector)'Old + and Context_Cursor (Ctx, F_Header) = Context_Cursor (Ctx, F_Header)'Old, + Contract_Cases => + (Structural_Valid (Ctx, F_Vector) => + True, + others => + True); + + procedure Update_Vector (Ctx : in out Context; Seq_Ctx : in out Modular_Vector_Sequence.Context) with + Pre => + Present (Ctx, F_Vector) + and then not Has_Buffer (Ctx) + and then Modular_Vector_Sequence.Has_Buffer (Seq_Ctx) + and then Ctx.Buffer_First = Seq_Ctx.Buffer_First + and then Ctx.Buffer_Last = Seq_Ctx.Buffer_Last + and then Seq_Ctx.First = Field_First (Ctx, F_Vector) + and then Seq_Ctx.Last = Field_Last (Ctx, F_Vector), + Post => + Present (Ctx, F_Vector) + and Has_Buffer (Ctx) + and not Modular_Vector_Sequence.Has_Buffer (Seq_Ctx) + and Seq_Ctx.First = Field_First (Ctx, F_Vector) + and Seq_Ctx.Last = Field_Last (Ctx, F_Vector) + and Seq_Ctx.First = Seq_Ctx.First'Old + and Seq_Ctx.Last = Seq_Ctx.Last'Old + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Field_First (Ctx, F_Vector) = Field_First (Ctx, F_Vector)'Old + and Field_Size (Ctx, F_Vector) = Field_Size (Ctx, F_Vector)'Old + and Context_Cursor (Ctx, F_Header) = Context_Cursor (Ctx, F_Header)'Old, + Depends => + (Ctx => (Ctx, Seq_Ctx), Seq_Ctx => Seq_Ctx); + + function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor with + Annotate => + (GNATprove, Inline_For_Proof), + Ghost; + + function Context_Cursors (Ctx : Context) return Field_Cursors with + Annotate => + (GNATprove, Inline_For_Proof), + Ghost; + +private + + type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + + function Valid_Value (Val : Field_Dependent_Value) return Boolean is + ((case Val.Fld is + when F_Header => + Valid (Val.Header_Value), + when F_Vector => + True, + when F_Initial | F_Final => + False)); + + type Field_Cursor (State : Cursor_State := S_Invalid) is + record + Predecessor : Virtual_Field := F_Final; + case State is + when S_Valid | S_Structural_Valid => + First : Types.Bit_Index := Types.Bit_Index'First; + Last : Types.Bit_Length := Types.Bit_Length'First; + Value : Field_Dependent_Value := (Fld => F_Final); + when S_Invalid | S_Incomplete => + null; + end case; + end record with + Dynamic_Predicate => + (if + State = S_Valid + or State = S_Structural_Valid + then + Valid_Value (Field_Cursor.Value)); + + type Field_Cursors is array (Virtual_Field) of Field_Cursor; + + function Structural_Valid (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Valid + or Cursor.State = S_Structural_Valid); + + function Valid (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Valid); + + function Invalid (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Invalid + or Cursor.State = S_Incomplete); + + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + ((if + Buffer /= null + then + Buffer'First = Buffer_First + and Buffer'Last = Buffer_Last) + and then (Types.Byte_Index (First) >= Buffer_First + and Types.Byte_Index (Last) <= Buffer_Last + and First <= Last + and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last + and then (for all F in Field'First .. Field'Last => + (if + Structural_Valid (Cursors (F)) + then + Cursors (F).First >= First + and Cursors (F).Last <= Message_Last + and Cursors (F).First <= Cursors (F).Last + 1 + and Cursors (F).Value.Fld = F)) + and then ((if + Structural_Valid (Cursors (F_Vector)) + then + (Valid (Cursors (F_Header)) + and then Cursors (F_Vector).Predecessor = F_Header))) + and then ((if + Invalid (Cursors (F_Header)) + then + Invalid (Cursors (F_Vector)))) + and then (if + Structural_Valid (Cursors (F_Header)) + then + Cursors (F_Header).Last - Cursors (F_Header).First + 1 = RFLX.Arrays.Enumeration_Base'Size + and then Cursors (F_Header).Predecessor = F_Initial + and then Cursors (F_Header).First = First + and then (if + Structural_Valid (Cursors (F_Vector)) + then + Cursors (F_Vector).Last - Cursors (F_Vector).First + 1 = Last - First + 1 - Types.Bit_Length (Cursors (F_Header).Last - Cursors (F_Header).First + 1) + and then Cursors (F_Vector).Predecessor = F_Header + and then Cursors (F_Vector).First = Cursors (F_Header).Last + 1))); + + type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is + record + Message_Last : Types.Bit_Index := First; + Buffer : Types.Bytes_Ptr := null; + Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); + end record with + Dynamic_Predicate => + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); + + function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is + (Ctx.Cursors (Fld)); + + function Context_Cursors (Ctx : Context) return Field_Cursors is + (Ctx.Cursors); + +end RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size; diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.adb b/tests/spark/generated/rflx-arrays-generic_inner_message.adb index 1710c6f568..b1cfd154cc 100644 --- a/tests/spark/generated/rflx-arrays-generic_inner_message.adb +++ b/tests/spark/generated/rflx-arrays-generic_inner_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Length) - and then Available_Space (Ctx, F_Length) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Length) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Length) and then Invalid (Ctx, F_Payload)); @@ -33,12 +33,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Payload)) - then - Ctx.Cursors (F_Payload).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -140,7 +135,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -254,6 +249,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -350,7 +346,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -359,6 +355,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -389,7 +386,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length); end Set_Length; @@ -399,7 +396,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Payload) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Payload), Predecessor => Ctx.Cursors (F_Payload).Predecessor); Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload); end Set_Payload_Empty; @@ -421,7 +418,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.ads b/tests/spark/generated/rflx-arrays-generic_inner_message.ads index 6f67e08e90..aef5625e19 100644 --- a/tests/spark/generated/rflx-arrays-generic_inner_message.ads +++ b/tests/spark/generated/rflx-arrays-generic_inner_message.ads @@ -56,6 +56,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -101,10 +102,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -215,6 +213,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old; @@ -234,6 +233,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Length (Ctx) = Get_Length (Ctx)'Old @@ -258,6 +258,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Length (Ctx) = Get_Length (Ctx)'Old @@ -278,6 +279,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Length (Ctx) = Get_Length (Ctx)'Old @@ -338,7 +340,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -348,12 +350,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -380,11 +384,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-arrays-generic_message.adb b/tests/spark/generated/rflx-arrays-generic_message.adb index 15d8083366..459b69b878 100644 --- a/tests/spark/generated/rflx-arrays-generic_message.adb +++ b/tests/spark/generated/rflx-arrays-generic_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Length) - and then Available_Space (Ctx, F_Length) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Length) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Length) and then Invalid (Ctx, F_Modular_Vector) and then Invalid (Ctx, F_Range_Vector) @@ -36,12 +36,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_AV_Enumeration_Vector)) - then - Ctx.Cursors (F_AV_Enumeration_Vector).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -221,7 +216,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -386,6 +381,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -539,7 +535,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -548,6 +544,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -578,7 +575,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length); end Set_Length; @@ -588,7 +585,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Modular_Vector); begin Reset_Dependent_Fields (Ctx, F_Modular_Vector); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Modular_Vector) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Modular_Vector), Predecessor => Ctx.Cursors (F_Modular_Vector).Predecessor); Ctx.Cursors (Successor (Ctx, F_Modular_Vector)) := (State => S_Invalid, Predecessor => F_Modular_Vector); end Set_Modular_Vector_Empty; @@ -600,7 +597,7 @@ is begin if Invalid (Ctx, F_Modular_Vector) then Reset_Dependent_Fields (Ctx, F_Modular_Vector); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then @@ -647,7 +644,7 @@ is begin if Invalid (Ctx, F_Range_Vector) then Reset_Dependent_Fields (Ctx, F_Range_Vector); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then @@ -694,7 +691,7 @@ is begin if Invalid (Ctx, F_Enumeration_Vector) then Reset_Dependent_Fields (Ctx, F_Enumeration_Vector); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then @@ -741,7 +738,7 @@ is begin if Invalid (Ctx, F_AV_Enumeration_Vector) then Reset_Dependent_Fields (Ctx, F_AV_Enumeration_Vector); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then diff --git a/tests/spark/generated/rflx-arrays-generic_message.ads b/tests/spark/generated/rflx-arrays-generic_message.ads index 5794c06bb2..f7c69fe2ff 100644 --- a/tests/spark/generated/rflx-arrays-generic_message.ads +++ b/tests/spark/generated/rflx-arrays-generic_message.ads @@ -61,6 +61,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -106,10 +107,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -244,6 +242,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old; @@ -268,6 +267,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Modular_Vector) = Predecessor (Ctx, F_Modular_Vector)'Old and Valid_Next (Ctx, F_Modular_Vector) = Valid_Next (Ctx, F_Modular_Vector)'Old and Get_Length (Ctx) = Get_Length (Ctx)'Old @@ -582,7 +582,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -592,12 +592,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -669,11 +671,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.adb b/tests/spark/generated/rflx-arrays-generic_messages_message.adb index 65fcdbd242..6523ec9114 100644 --- a/tests/spark/generated/rflx-arrays-generic_messages_message.adb +++ b/tests/spark/generated/rflx-arrays-generic_messages_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Length => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Length) - and then Available_Space (Ctx, F_Length) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Length) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Length) and then Invalid (Ctx, F_Messages)); @@ -33,12 +33,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Messages)) - then - Ctx.Cursors (F_Messages).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -140,7 +135,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -254,6 +249,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -350,7 +346,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -359,6 +355,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -389,7 +386,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length); end Set_Length; @@ -399,7 +396,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Messages); begin Reset_Dependent_Fields (Ctx, F_Messages); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Messages) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Messages), Predecessor => Ctx.Cursors (F_Messages).Predecessor); Ctx.Cursors (Successor (Ctx, F_Messages)) := (State => S_Invalid, Predecessor => F_Messages); end Set_Messages_Empty; @@ -411,7 +408,7 @@ is begin if Invalid (Ctx, F_Messages) then Reset_Dependent_Fields (Ctx, F_Messages); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Length)) then diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.ads b/tests/spark/generated/rflx-arrays-generic_messages_message.ads index bafd108f47..bb174a5a08 100644 --- a/tests/spark/generated/rflx-arrays-generic_messages_message.ads +++ b/tests/spark/generated/rflx-arrays-generic_messages_message.ads @@ -58,6 +58,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -103,10 +104,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -217,6 +215,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old; @@ -236,6 +235,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Messages) = Predecessor (Ctx, F_Messages)'Old and Valid_Next (Ctx, F_Messages) = Valid_Next (Ctx, F_Messages)'Old and Get_Length (Ctx) = Get_Length (Ctx)'Old @@ -352,7 +352,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -362,12 +362,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -394,11 +396,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-enumeration-generic_message.adb b/tests/spark/generated/rflx-enumeration-generic_message.adb index bf25211c1b..4b1fd32f6d 100644 --- a/tests/spark/generated/rflx-enumeration-generic_message.adb +++ b/tests/spark/generated/rflx-enumeration-generic_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Priority => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Priority => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Priority) - and then Available_Space (Ctx, F_Priority) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Priority) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Priority)); procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr) is @@ -32,12 +32,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Priority)) - then - Ctx.Cursors (F_Priority).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -104,7 +99,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -196,6 +191,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -273,7 +269,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -282,6 +278,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -312,7 +309,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Priority); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Priority) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Priority).Predecessor); Ctx.Cursors (Successor (Ctx, F_Priority)) := (State => S_Invalid, Predecessor => F_Priority); end Set_Priority; diff --git a/tests/spark/generated/rflx-enumeration-generic_message.ads b/tests/spark/generated/rflx-enumeration-generic_message.ads index d7eddc095c..1a31362855 100644 --- a/tests/spark/generated/rflx-enumeration-generic_message.ads +++ b/tests/spark/generated/rflx-enumeration-generic_message.ads @@ -56,6 +56,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -101,10 +102,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -200,6 +198,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Priority) = Predecessor (Ctx, F_Priority)'Old and Valid_Next (Ctx, F_Priority) = Valid_Next (Ctx, F_Priority)'Old; @@ -256,7 +255,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -266,12 +265,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then (True) @@ -285,11 +286,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-ethernet-generic_frame.adb b/tests/spark/generated/rflx-ethernet-generic_frame.adb index df09d3e492..31b3a6af08 100644 --- a/tests/spark/generated/rflx-ethernet-generic_frame.adb +++ b/tests/spark/generated/rflx-ethernet-generic_frame.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Destination => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Destination => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Destination) - and then Available_Space (Ctx, F_Destination) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Destination) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Destination) and then Invalid (Ctx, F_Source) and then Invalid (Ctx, F_Type_Length_TPID) @@ -38,14 +38,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then (Types.U64 (Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1) / 8 >= 46 - and Types.U64 (Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1) / 8 <= 1500) - then - Ctx.Cursors (F_Payload).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -341,7 +334,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -558,6 +551,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value, Field_Size (Ctx, Fld)) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -795,7 +789,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -804,6 +798,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -847,7 +842,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Destination); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Destination) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Destination).Predecessor); Ctx.Cursors (Successor (Ctx, F_Destination)) := (State => S_Invalid, Predecessor => F_Destination); end Set_Destination; @@ -858,7 +853,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Source); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Source) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Source).Predecessor); Ctx.Cursors (Successor (Ctx, F_Source)) := (State => S_Invalid, Predecessor => F_Source); end Set_Source; @@ -869,7 +864,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Type_Length_TPID); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Type_Length_TPID) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Type_Length_TPID).Predecessor); Ctx.Cursors (Successor (Ctx, F_Type_Length_TPID)) := (State => S_Invalid, Predecessor => F_Type_Length_TPID); end Set_Type_Length_TPID; @@ -880,7 +875,7 @@ is begin Reset_Dependent_Fields (Ctx, F_TPID); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_TPID) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_TPID).Predecessor); Ctx.Cursors (Successor (Ctx, F_TPID)) := (State => S_Invalid, Predecessor => F_TPID); end Set_TPID; @@ -891,7 +886,7 @@ is begin Reset_Dependent_Fields (Ctx, F_TCI); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_TCI) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_TCI).Predecessor); Ctx.Cursors (Successor (Ctx, F_TCI)) := (State => S_Invalid, Predecessor => F_TCI); end Set_TCI; @@ -902,7 +897,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Type_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Type_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Type_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Type_Length)) := (State => S_Invalid, Predecessor => F_Type_Length); end Set_Type_Length; @@ -919,24 +914,12 @@ is Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last)); end Set_Payload; - procedure Set_Bounded_Payload (Ctx : in out Context; Size : Types.Bit_Length) is - First : constant Types.Bit_Index := Field_First (Ctx, F_Payload); - Last : constant Types.Bit_Index := First + Size - 1; - function Buffer_First return Types.Index is - (Types.Byte_Index (First)); - function Buffer_Last return Types.Index is - (Types.Byte_Index (Last)); - begin - Initialize_Bounded_Payload (Ctx, Size); - Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last)); - end Set_Bounded_Payload; - procedure Initialize_Payload (Ctx : in out Context) is First : constant Types.Bit_Index := Field_First (Ctx, F_Payload); Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Destination)) then @@ -1013,86 +996,4 @@ is Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload); end Initialize_Payload; - procedure Initialize_Bounded_Payload (Ctx : in out Context; Size : Types.Bit_Length) is - First : constant Types.Bit_Index := Field_First (Ctx, F_Payload); - Last : constant Types.Bit_Index := First + Size - 1; - begin - Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); - pragma Assert ((if - Structural_Valid (Ctx.Cursors (F_Destination)) - then - Ctx.Cursors (F_Destination).Last - Ctx.Cursors (F_Destination).First + 1 = RFLX.Ethernet.Address'Size - and then Ctx.Cursors (F_Destination).Predecessor = F_Initial - and then Ctx.Cursors (F_Destination).First = Ctx.First - and then (if - Structural_Valid (Ctx.Cursors (F_Source)) - then - Ctx.Cursors (F_Source).Last - Ctx.Cursors (F_Source).First + 1 = RFLX.Ethernet.Address'Size - and then Ctx.Cursors (F_Source).Predecessor = F_Destination - and then Ctx.Cursors (F_Source).First = Ctx.Cursors (F_Destination).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Type_Length_TPID)) - then - Ctx.Cursors (F_Type_Length_TPID).Last - Ctx.Cursors (F_Type_Length_TPID).First + 1 = RFLX.Ethernet.Type_Length_Base'Size - and then Ctx.Cursors (F_Type_Length_TPID).Predecessor = F_Source - and then Ctx.Cursors (F_Type_Length_TPID).First = Ctx.Cursors (F_Source).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_TPID)) - and then Ctx.Cursors (F_Type_Length_TPID).Value.Type_Length_TPID_Value = 16#8100# - then - Ctx.Cursors (F_TPID).Last - Ctx.Cursors (F_TPID).First + 1 = RFLX.Ethernet.TPID_Base'Size - and then Ctx.Cursors (F_TPID).Predecessor = F_Type_Length_TPID - and then Ctx.Cursors (F_TPID).First = Ctx.Cursors (F_Type_Length_TPID).First - and then (if - Structural_Valid (Ctx.Cursors (F_TCI)) - then - Ctx.Cursors (F_TCI).Last - Ctx.Cursors (F_TCI).First + 1 = RFLX.Ethernet.TCI'Size - and then Ctx.Cursors (F_TCI).Predecessor = F_TPID - and then Ctx.Cursors (F_TCI).First = Ctx.Cursors (F_TPID).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Type_Length)) - then - Ctx.Cursors (F_Type_Length).Last - Ctx.Cursors (F_Type_Length).First + 1 = RFLX.Ethernet.Type_Length_Base'Size - and then Ctx.Cursors (F_Type_Length).Predecessor = F_TCI - and then Ctx.Cursors (F_Type_Length).First = Ctx.Cursors (F_TCI).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then Ctx.Cursors (F_Type_Length).Value.Type_Length_Value <= 1500 - then - Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1 = Types.Bit_Length (Ctx.Cursors (F_Type_Length).Value.Type_Length_Value) * 8 - and then Ctx.Cursors (F_Payload).Predecessor = F_Type_Length - and then Ctx.Cursors (F_Payload).First = Ctx.Cursors (F_Type_Length).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then Ctx.Cursors (F_Type_Length).Value.Type_Length_Value >= 1536 - then - Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1 = Ctx.Last - Ctx.Cursors (F_Type_Length).Last - and then Ctx.Cursors (F_Payload).Predecessor = F_Type_Length - and then Ctx.Cursors (F_Payload).First = Ctx.Cursors (F_Type_Length).Last + 1)))) - and then (if - Structural_Valid (Ctx.Cursors (F_Type_Length)) - and then Ctx.Cursors (F_Type_Length_TPID).Value.Type_Length_TPID_Value /= 16#8100# - then - Ctx.Cursors (F_Type_Length).Last - Ctx.Cursors (F_Type_Length).First + 1 = RFLX.Ethernet.Type_Length_Base'Size - and then Ctx.Cursors (F_Type_Length).Predecessor = F_Type_Length_TPID - and then Ctx.Cursors (F_Type_Length).First = Ctx.Cursors (F_Type_Length_TPID).First - and then (if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then Ctx.Cursors (F_Type_Length).Value.Type_Length_Value <= 1500 - then - Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1 = Types.Bit_Length (Ctx.Cursors (F_Type_Length).Value.Type_Length_Value) * 8 - and then Ctx.Cursors (F_Payload).Predecessor = F_Type_Length - and then Ctx.Cursors (F_Payload).First = Ctx.Cursors (F_Type_Length).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then Ctx.Cursors (F_Type_Length).Value.Type_Length_Value >= 1536 - then - Ctx.Cursors (F_Payload).Last - Ctx.Cursors (F_Payload).First + 1 = Ctx.Last - Ctx.Cursors (F_Type_Length).Last - and then Ctx.Cursors (F_Payload).Predecessor = F_Type_Length - and then Ctx.Cursors (F_Payload).First = Ctx.Cursors (F_Type_Length).Last + 1)))))); - Ctx.Cursors (F_Payload) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Payload), Predecessor => Ctx.Cursors (F_Payload).Predecessor); - Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload); - end Initialize_Bounded_Payload; - end RFLX.Ethernet.Generic_Frame; diff --git a/tests/spark/generated/rflx-ethernet-generic_frame.ads b/tests/spark/generated/rflx-ethernet-generic_frame.ads index 5269960934..1918049f43 100644 --- a/tests/spark/generated/rflx-ethernet-generic_frame.ads +++ b/tests/spark/generated/rflx-ethernet-generic_frame.ads @@ -66,6 +66,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -111,10 +112,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -250,6 +248,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Destination) = Predecessor (Ctx, F_Destination)'Old and Valid_Next (Ctx, F_Destination) = Valid_Next (Ctx, F_Destination)'Old; @@ -276,6 +275,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Source) = Predecessor (Ctx, F_Source)'Old and Valid_Next (Ctx, F_Source) = Valid_Next (Ctx, F_Source)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -311,6 +311,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Type_Length_TPID) = Predecessor (Ctx, F_Type_Length_TPID)'Old and Valid_Next (Ctx, F_Type_Length_TPID) = Valid_Next (Ctx, F_Type_Length_TPID)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -339,6 +340,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_TPID) = Predecessor (Ctx, F_TPID)'Old and Valid_Next (Ctx, F_TPID) = Valid_Next (Ctx, F_TPID)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -368,6 +370,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_TCI) = Predecessor (Ctx, F_TCI)'Old and Valid_Next (Ctx, F_TCI) = Valid_Next (Ctx, F_TCI)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -406,6 +409,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Type_Length) = Predecessor (Ctx, F_Type_Length)'Old and Valid_Next (Ctx, F_Type_Length) = Valid_Next (Ctx, F_Type_Length)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -436,36 +440,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old - and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old - and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old - and Get_Destination (Ctx) = Get_Destination (Ctx)'Old - and Get_Source (Ctx) = Get_Source (Ctx)'Old - and Get_Type_Length_TPID (Ctx) = Get_Type_Length_TPID (Ctx)'Old - and Get_Type_Length (Ctx) = Get_Type_Length (Ctx)'Old - and Structural_Valid (Ctx, F_Payload); - - generic - with procedure Process_Payload (Payload : out Types.Bytes); - with function Valid_Length (Length : Types.Length) return Boolean; - procedure Set_Bounded_Payload (Ctx : in out Context; Size : Types.Bit_Length) with - Pre => - not Ctx'Constrained - and then Has_Buffer (Ctx) - and then Valid_Next (Ctx, F_Payload) - and then Field_Last (Ctx, F_Payload) <= Types.Bit_Index'Last / 2 - and then Field_Condition (Ctx, (Fld => F_Payload), Size) - and then Available_Space (Ctx, F_Payload) >= Size - and then Field_First (Ctx, F_Payload) + Size <= Types.Bit_Index'Last / 2 - and then ((Valid (Ctx, F_Type_Length) - and Get_Type_Length (Ctx) >= 1536)) - and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1 - and then Size mod Types.Byte'Size = 0 - and then Valid_Length (Types.Length (Size / Types.Byte'Size)), - Post => - Has_Buffer (Ctx) - and Ctx.Buffer_First = Ctx.Buffer_First'Old - and Ctx.Buffer_Last = Ctx.Buffer_Last'Old - and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -489,32 +464,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old - and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old - and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old - and Get_Destination (Ctx) = Get_Destination (Ctx)'Old - and Get_Source (Ctx) = Get_Source (Ctx)'Old - and Get_Type_Length_TPID (Ctx) = Get_Type_Length_TPID (Ctx)'Old - and Get_Type_Length (Ctx) = Get_Type_Length (Ctx)'Old - and Structural_Valid (Ctx, F_Payload); - - procedure Initialize_Bounded_Payload (Ctx : in out Context; Size : Types.Bit_Length) with - Pre => - not Ctx'Constrained - and then Has_Buffer (Ctx) - and then Valid_Next (Ctx, F_Payload) - and then Field_Last (Ctx, F_Payload) <= Types.Bit_Index'Last / 2 - and then Field_Condition (Ctx, (Fld => F_Payload), Size) - and then Available_Space (Ctx, F_Payload) >= Size - and then Field_First (Ctx, F_Payload) + Size <= Types.Bit_Index'Last / 2 - and then ((Valid (Ctx, F_Type_Length) - and Get_Type_Length (Ctx) >= 1536)) - and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1 - and then Size mod Types.Byte'Size = 0, - Post => - Has_Buffer (Ctx) - and Ctx.Buffer_First = Ctx.Buffer_First'Old - and Ctx.Buffer_Last = Ctx.Buffer_Last'Old - and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Destination (Ctx) = Get_Destination (Ctx)'Old @@ -588,7 +538,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -598,12 +548,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -744,11 +696,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-expression-generic_message.adb b/tests/spark/generated/rflx-expression-generic_message.adb index e2b276e59a..e74d4dac61 100644 --- a/tests/spark/generated/rflx-expression-generic_message.adb +++ b/tests/spark/generated/rflx-expression-generic_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Payload => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Payload => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Payload) - and then Available_Space (Ctx, F_Payload) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Payload) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Payload)); procedure Take_Buffer (Ctx : in out Context; Buffer : out Types.Bytes_Ptr) is @@ -32,13 +32,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Payload)) - and then Equal (Ctx, F_Payload, (Types.Byte'Val (1), Types.Byte'Val (2))) - then - Ctx.Cursors (F_Payload).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -112,7 +106,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -201,6 +195,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -283,7 +278,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Payload)) then diff --git a/tests/spark/generated/rflx-expression-generic_message.ads b/tests/spark/generated/rflx-expression-generic_message.ads index 4583e3fe05..0a4cea08f6 100644 --- a/tests/spark/generated/rflx-expression-generic_message.ads +++ b/tests/spark/generated/rflx-expression-generic_message.ads @@ -54,6 +54,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -99,10 +100,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -209,6 +207,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Structural_Valid (Ctx, F_Payload); @@ -228,6 +227,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Structural_Valid (Ctx, F_Payload); @@ -285,7 +285,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -295,12 +295,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then (True) @@ -314,11 +316,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-icmp-generic_message.adb b/tests/spark/generated/rflx-icmp-generic_message.adb index c6a67a598a..75b3531c1c 100644 --- a/tests/spark/generated/rflx-icmp-generic_message.adb +++ b/tests/spark/generated/rflx-icmp-generic_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Tag => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Tag => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Tag) - and then Available_Space (Ctx, F_Tag) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Tag) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Tag) and then Invalid (Ctx, F_Code_Destination_Unreachable) and then Invalid (Ctx, F_Code_Redirect) @@ -47,22 +47,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - elsif - Structural_Valid (Ctx.Cursors (F_Sequence_Number)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply))) - then - Ctx.Cursors (F_Sequence_Number).Last - elsif - Structural_Valid (Ctx.Cursors (F_Transmit_Timestamp)) - then - Ctx.Cursors (F_Transmit_Timestamp).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -672,7 +657,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -1269,6 +1254,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -2164,7 +2150,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -2173,6 +2159,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -2245,7 +2232,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Tag); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Tag) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Tag).Predecessor); Ctx.Cursors (Successor (Ctx, F_Tag)) := (State => S_Invalid, Predecessor => F_Tag); end Set_Tag; @@ -2256,7 +2243,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Code_Destination_Unreachable); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Code_Destination_Unreachable) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Code_Destination_Unreachable).Predecessor); Ctx.Cursors (Successor (Ctx, F_Code_Destination_Unreachable)) := (State => S_Invalid, Predecessor => F_Code_Destination_Unreachable); end Set_Code_Destination_Unreachable; @@ -2267,7 +2254,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Code_Redirect); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Code_Redirect) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Code_Redirect).Predecessor); Ctx.Cursors (Successor (Ctx, F_Code_Redirect)) := (State => S_Invalid, Predecessor => F_Code_Redirect); end Set_Code_Redirect; @@ -2278,7 +2265,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Code_Time_Exceeded); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Code_Time_Exceeded) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Code_Time_Exceeded).Predecessor); Ctx.Cursors (Successor (Ctx, F_Code_Time_Exceeded)) := (State => S_Invalid, Predecessor => F_Code_Time_Exceeded); end Set_Code_Time_Exceeded; @@ -2289,7 +2276,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Code_Zero); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Code_Zero) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Code_Zero).Predecessor); Ctx.Cursors (Successor (Ctx, F_Code_Zero)) := (State => S_Invalid, Predecessor => F_Code_Zero); end Set_Code_Zero; @@ -2300,7 +2287,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Checksum); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Checksum) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Checksum).Predecessor); Ctx.Cursors (Successor (Ctx, F_Checksum)) := (State => S_Invalid, Predecessor => F_Checksum); end Set_Checksum; @@ -2311,7 +2298,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Gateway_Internet_Address); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Gateway_Internet_Address) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Gateway_Internet_Address).Predecessor); Ctx.Cursors (Successor (Ctx, F_Gateway_Internet_Address)) := (State => S_Invalid, Predecessor => F_Gateway_Internet_Address); end Set_Gateway_Internet_Address; @@ -2322,7 +2309,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Identifier); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Identifier) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Identifier).Predecessor); Ctx.Cursors (Successor (Ctx, F_Identifier)) := (State => S_Invalid, Predecessor => F_Identifier); end Set_Identifier; @@ -2333,7 +2320,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Pointer); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Pointer) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Pointer).Predecessor); Ctx.Cursors (Successor (Ctx, F_Pointer)) := (State => S_Invalid, Predecessor => F_Pointer); end Set_Pointer; @@ -2344,7 +2331,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Unused_32); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Unused_32) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Unused_32).Predecessor); Ctx.Cursors (Successor (Ctx, F_Unused_32)) := (State => S_Invalid, Predecessor => F_Unused_32); end Set_Unused_32; @@ -2355,7 +2342,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Sequence_Number); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Sequence_Number) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Sequence_Number).Predecessor); Ctx.Cursors (Successor (Ctx, F_Sequence_Number)) := (State => S_Invalid, Predecessor => F_Sequence_Number); end Set_Sequence_Number; @@ -2366,7 +2353,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Unused_24); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Unused_24) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Unused_24).Predecessor); Ctx.Cursors (Successor (Ctx, F_Unused_24)) := (State => S_Invalid, Predecessor => F_Unused_24); end Set_Unused_24; @@ -2377,7 +2364,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Originate_Timestamp); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Originate_Timestamp) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Originate_Timestamp).Predecessor); Ctx.Cursors (Successor (Ctx, F_Originate_Timestamp)) := (State => S_Invalid, Predecessor => F_Originate_Timestamp); end Set_Originate_Timestamp; @@ -2388,7 +2375,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Receive_Timestamp); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Receive_Timestamp) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Receive_Timestamp).Predecessor); Ctx.Cursors (Successor (Ctx, F_Receive_Timestamp)) := (State => S_Invalid, Predecessor => F_Receive_Timestamp); end Set_Receive_Timestamp; @@ -2399,7 +2386,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Transmit_Timestamp); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Transmit_Timestamp) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Transmit_Timestamp).Predecessor); Ctx.Cursors (Successor (Ctx, F_Transmit_Timestamp)) := (State => S_Invalid, Predecessor => F_Transmit_Timestamp); end Set_Transmit_Timestamp; @@ -2409,7 +2396,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Data); begin Reset_Dependent_Fields (Ctx, F_Data); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Data) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor); Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data); end Set_Data_Empty; @@ -2426,24 +2413,12 @@ is Process_Data (Ctx.Buffer.all (Buffer_First .. Buffer_Last)); end Set_Data; - procedure Set_Bounded_Data (Ctx : in out Context; Size : Types.Bit_Length) is - First : constant Types.Bit_Index := Field_First (Ctx, F_Data); - Last : constant Types.Bit_Index := First + Size - 1; - function Buffer_First return Types.Index is - (Types.Byte_Index (First)); - function Buffer_Last return Types.Index is - (Types.Byte_Index (Last)); - begin - Initialize_Bounded_Data (Ctx, Size); - Process_Data (Ctx.Buffer.all (Buffer_First .. Buffer_Last)); - end Set_Bounded_Data; - procedure Initialize_Data (Ctx : in out Context) is First : constant Types.Bit_Index := Field_First (Ctx, F_Data); Last : constant Types.Bit_Index := Field_Last (Ctx, F_Data); begin Reset_Dependent_Fields (Ctx, F_Data); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Tag)) then @@ -2885,451 +2860,4 @@ is Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data); end Initialize_Data; - procedure Initialize_Bounded_Data (Ctx : in out Context; Size : Types.Bit_Length) is - First : constant Types.Bit_Index := Field_First (Ctx, F_Data); - Last : constant Types.Bit_Index := First + Size - 1; - begin - Reset_Dependent_Fields (Ctx, F_Data); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); - pragma Assert ((if - Structural_Valid (Ctx.Cursors (F_Tag)) - then - Ctx.Cursors (F_Tag).Last - Ctx.Cursors (F_Tag).First + 1 = RFLX.ICMP.Tag_Base'Size - and then Ctx.Cursors (F_Tag).Predecessor = F_Initial - and then Ctx.Cursors (F_Tag).First = Ctx.First - and then (if - Structural_Valid (Ctx.Cursors (F_Code_Destination_Unreachable)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Destination_Unreachable)) - then - Ctx.Cursors (F_Code_Destination_Unreachable).Last - Ctx.Cursors (F_Code_Destination_Unreachable).First + 1 = RFLX.ICMP.Code_Destination_Unreachable_Base'Size - and then Ctx.Cursors (F_Code_Destination_Unreachable).Predecessor = F_Tag - and then Ctx.Cursors (F_Code_Destination_Unreachable).First = Ctx.Cursors (F_Tag).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Checksum)) - then - Ctx.Cursors (F_Checksum).Last - Ctx.Cursors (F_Checksum).First + 1 = RFLX.ICMP.Checksum'Size - and then Ctx.Cursors (F_Checksum).Predecessor = F_Code_Destination_Unreachable - and then Ctx.Cursors (F_Checksum).First = Ctx.Cursors (F_Code_Destination_Unreachable).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Gateway_Internet_Address)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Redirect)) - then - Ctx.Cursors (F_Gateway_Internet_Address).Last - Ctx.Cursors (F_Gateway_Internet_Address).First + 1 = RFLX.ICMP.Gateway_Internet_Address'Size - and then Ctx.Cursors (F_Gateway_Internet_Address).Predecessor = F_Checksum - and then Ctx.Cursors (F_Gateway_Internet_Address).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Gateway_Internet_Address - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Gateway_Internet_Address).Last + 1)) - and then (if - Structural_Valid (Ctx.Cursors (F_Identifier)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply))) - then - Ctx.Cursors (F_Identifier).Last - Ctx.Cursors (F_Identifier).First + 1 = RFLX.ICMP.Identifier'Size - and then Ctx.Cursors (F_Identifier).Predecessor = F_Checksum - and then Ctx.Cursors (F_Identifier).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Sequence_Number)) - then - Ctx.Cursors (F_Sequence_Number).Last - Ctx.Cursors (F_Sequence_Number).First + 1 = RFLX.ICMP.Sequence_Number'Size - and then Ctx.Cursors (F_Sequence_Number).Predecessor = F_Identifier - and then Ctx.Cursors (F_Sequence_Number).First = Ctx.Cursors (F_Identifier).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request))) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = Ctx.Last - Ctx.Cursors (F_Sequence_Number).Last - and then Ctx.Cursors (F_Data).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Sequence_Number).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Originate_Timestamp)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply))) - then - Ctx.Cursors (F_Originate_Timestamp).Last - Ctx.Cursors (F_Originate_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Originate_Timestamp).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Originate_Timestamp).First = Ctx.Cursors (F_Sequence_Number).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Receive_Timestamp)) - then - Ctx.Cursors (F_Receive_Timestamp).Last - Ctx.Cursors (F_Receive_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Receive_Timestamp).Predecessor = F_Originate_Timestamp - and then Ctx.Cursors (F_Receive_Timestamp).First = Ctx.Cursors (F_Originate_Timestamp).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Transmit_Timestamp)) - then - Ctx.Cursors (F_Transmit_Timestamp).Last - Ctx.Cursors (F_Transmit_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Transmit_Timestamp).Predecessor = F_Receive_Timestamp - and then Ctx.Cursors (F_Transmit_Timestamp).First = Ctx.Cursors (F_Receive_Timestamp).Last + 1))))) - and then (if - Structural_Valid (Ctx.Cursors (F_Pointer)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Parameter_Problem)) - then - Ctx.Cursors (F_Pointer).Last - Ctx.Cursors (F_Pointer).First + 1 = RFLX.ICMP.Pointer'Size - and then Ctx.Cursors (F_Pointer).Predecessor = F_Checksum - and then Ctx.Cursors (F_Pointer).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_24)) - then - Ctx.Cursors (F_Unused_24).Last - Ctx.Cursors (F_Unused_24).First + 1 = RFLX.ICMP.Unused_24_Base'Size - and then Ctx.Cursors (F_Unused_24).Predecessor = F_Pointer - and then Ctx.Cursors (F_Unused_24).First = Ctx.Cursors (F_Pointer).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_24 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_24).Last + 1))) - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_32)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Time_Exceeded)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Destination_Unreachable)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Source_Quench))) - then - Ctx.Cursors (F_Unused_32).Last - Ctx.Cursors (F_Unused_32).First + 1 = RFLX.ICMP.Unused_32_Base'Size - and then Ctx.Cursors (F_Unused_32).Predecessor = F_Checksum - and then Ctx.Cursors (F_Unused_32).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_32 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_32).Last + 1)))) - and then (if - Structural_Valid (Ctx.Cursors (F_Code_Redirect)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Redirect)) - then - Ctx.Cursors (F_Code_Redirect).Last - Ctx.Cursors (F_Code_Redirect).First + 1 = RFLX.ICMP.Code_Redirect_Base'Size - and then Ctx.Cursors (F_Code_Redirect).Predecessor = F_Tag - and then Ctx.Cursors (F_Code_Redirect).First = Ctx.Cursors (F_Tag).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Checksum)) - then - Ctx.Cursors (F_Checksum).Last - Ctx.Cursors (F_Checksum).First + 1 = RFLX.ICMP.Checksum'Size - and then Ctx.Cursors (F_Checksum).Predecessor = F_Code_Redirect - and then Ctx.Cursors (F_Checksum).First = Ctx.Cursors (F_Code_Redirect).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Gateway_Internet_Address)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Redirect)) - then - Ctx.Cursors (F_Gateway_Internet_Address).Last - Ctx.Cursors (F_Gateway_Internet_Address).First + 1 = RFLX.ICMP.Gateway_Internet_Address'Size - and then Ctx.Cursors (F_Gateway_Internet_Address).Predecessor = F_Checksum - and then Ctx.Cursors (F_Gateway_Internet_Address).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Gateway_Internet_Address - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Gateway_Internet_Address).Last + 1)) - and then (if - Structural_Valid (Ctx.Cursors (F_Identifier)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply))) - then - Ctx.Cursors (F_Identifier).Last - Ctx.Cursors (F_Identifier).First + 1 = RFLX.ICMP.Identifier'Size - and then Ctx.Cursors (F_Identifier).Predecessor = F_Checksum - and then Ctx.Cursors (F_Identifier).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Sequence_Number)) - then - Ctx.Cursors (F_Sequence_Number).Last - Ctx.Cursors (F_Sequence_Number).First + 1 = RFLX.ICMP.Sequence_Number'Size - and then Ctx.Cursors (F_Sequence_Number).Predecessor = F_Identifier - and then Ctx.Cursors (F_Sequence_Number).First = Ctx.Cursors (F_Identifier).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request))) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = Ctx.Last - Ctx.Cursors (F_Sequence_Number).Last - and then Ctx.Cursors (F_Data).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Sequence_Number).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Originate_Timestamp)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply))) - then - Ctx.Cursors (F_Originate_Timestamp).Last - Ctx.Cursors (F_Originate_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Originate_Timestamp).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Originate_Timestamp).First = Ctx.Cursors (F_Sequence_Number).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Receive_Timestamp)) - then - Ctx.Cursors (F_Receive_Timestamp).Last - Ctx.Cursors (F_Receive_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Receive_Timestamp).Predecessor = F_Originate_Timestamp - and then Ctx.Cursors (F_Receive_Timestamp).First = Ctx.Cursors (F_Originate_Timestamp).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Transmit_Timestamp)) - then - Ctx.Cursors (F_Transmit_Timestamp).Last - Ctx.Cursors (F_Transmit_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Transmit_Timestamp).Predecessor = F_Receive_Timestamp - and then Ctx.Cursors (F_Transmit_Timestamp).First = Ctx.Cursors (F_Receive_Timestamp).Last + 1))))) - and then (if - Structural_Valid (Ctx.Cursors (F_Pointer)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Parameter_Problem)) - then - Ctx.Cursors (F_Pointer).Last - Ctx.Cursors (F_Pointer).First + 1 = RFLX.ICMP.Pointer'Size - and then Ctx.Cursors (F_Pointer).Predecessor = F_Checksum - and then Ctx.Cursors (F_Pointer).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_24)) - then - Ctx.Cursors (F_Unused_24).Last - Ctx.Cursors (F_Unused_24).First + 1 = RFLX.ICMP.Unused_24_Base'Size - and then Ctx.Cursors (F_Unused_24).Predecessor = F_Pointer - and then Ctx.Cursors (F_Unused_24).First = Ctx.Cursors (F_Pointer).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_24 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_24).Last + 1))) - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_32)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Time_Exceeded)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Destination_Unreachable)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Source_Quench))) - then - Ctx.Cursors (F_Unused_32).Last - Ctx.Cursors (F_Unused_32).First + 1 = RFLX.ICMP.Unused_32_Base'Size - and then Ctx.Cursors (F_Unused_32).Predecessor = F_Checksum - and then Ctx.Cursors (F_Unused_32).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_32 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_32).Last + 1)))) - and then (if - Structural_Valid (Ctx.Cursors (F_Code_Time_Exceeded)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Time_Exceeded)) - then - Ctx.Cursors (F_Code_Time_Exceeded).Last - Ctx.Cursors (F_Code_Time_Exceeded).First + 1 = RFLX.ICMP.Code_Time_Exceeded_Base'Size - and then Ctx.Cursors (F_Code_Time_Exceeded).Predecessor = F_Tag - and then Ctx.Cursors (F_Code_Time_Exceeded).First = Ctx.Cursors (F_Tag).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Checksum)) - then - Ctx.Cursors (F_Checksum).Last - Ctx.Cursors (F_Checksum).First + 1 = RFLX.ICMP.Checksum'Size - and then Ctx.Cursors (F_Checksum).Predecessor = F_Code_Time_Exceeded - and then Ctx.Cursors (F_Checksum).First = Ctx.Cursors (F_Code_Time_Exceeded).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Gateway_Internet_Address)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Redirect)) - then - Ctx.Cursors (F_Gateway_Internet_Address).Last - Ctx.Cursors (F_Gateway_Internet_Address).First + 1 = RFLX.ICMP.Gateway_Internet_Address'Size - and then Ctx.Cursors (F_Gateway_Internet_Address).Predecessor = F_Checksum - and then Ctx.Cursors (F_Gateway_Internet_Address).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Gateway_Internet_Address - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Gateway_Internet_Address).Last + 1)) - and then (if - Structural_Valid (Ctx.Cursors (F_Identifier)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply))) - then - Ctx.Cursors (F_Identifier).Last - Ctx.Cursors (F_Identifier).First + 1 = RFLX.ICMP.Identifier'Size - and then Ctx.Cursors (F_Identifier).Predecessor = F_Checksum - and then Ctx.Cursors (F_Identifier).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Sequence_Number)) - then - Ctx.Cursors (F_Sequence_Number).Last - Ctx.Cursors (F_Sequence_Number).First + 1 = RFLX.ICMP.Sequence_Number'Size - and then Ctx.Cursors (F_Sequence_Number).Predecessor = F_Identifier - and then Ctx.Cursors (F_Sequence_Number).First = Ctx.Cursors (F_Identifier).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request))) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = Ctx.Last - Ctx.Cursors (F_Sequence_Number).Last - and then Ctx.Cursors (F_Data).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Sequence_Number).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Originate_Timestamp)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply))) - then - Ctx.Cursors (F_Originate_Timestamp).Last - Ctx.Cursors (F_Originate_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Originate_Timestamp).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Originate_Timestamp).First = Ctx.Cursors (F_Sequence_Number).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Receive_Timestamp)) - then - Ctx.Cursors (F_Receive_Timestamp).Last - Ctx.Cursors (F_Receive_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Receive_Timestamp).Predecessor = F_Originate_Timestamp - and then Ctx.Cursors (F_Receive_Timestamp).First = Ctx.Cursors (F_Originate_Timestamp).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Transmit_Timestamp)) - then - Ctx.Cursors (F_Transmit_Timestamp).Last - Ctx.Cursors (F_Transmit_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Transmit_Timestamp).Predecessor = F_Receive_Timestamp - and then Ctx.Cursors (F_Transmit_Timestamp).First = Ctx.Cursors (F_Receive_Timestamp).Last + 1))))) - and then (if - Structural_Valid (Ctx.Cursors (F_Pointer)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Parameter_Problem)) - then - Ctx.Cursors (F_Pointer).Last - Ctx.Cursors (F_Pointer).First + 1 = RFLX.ICMP.Pointer'Size - and then Ctx.Cursors (F_Pointer).Predecessor = F_Checksum - and then Ctx.Cursors (F_Pointer).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_24)) - then - Ctx.Cursors (F_Unused_24).Last - Ctx.Cursors (F_Unused_24).First + 1 = RFLX.ICMP.Unused_24_Base'Size - and then Ctx.Cursors (F_Unused_24).Predecessor = F_Pointer - and then Ctx.Cursors (F_Unused_24).First = Ctx.Cursors (F_Pointer).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_24 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_24).Last + 1))) - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_32)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Time_Exceeded)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Destination_Unreachable)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Source_Quench))) - then - Ctx.Cursors (F_Unused_32).Last - Ctx.Cursors (F_Unused_32).First + 1 = RFLX.ICMP.Unused_32_Base'Size - and then Ctx.Cursors (F_Unused_32).Predecessor = F_Checksum - and then Ctx.Cursors (F_Unused_32).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_32 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_32).Last + 1)))) - and then (if - Structural_Valid (Ctx.Cursors (F_Code_Zero)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Parameter_Problem)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Source_Quench)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request))) - then - Ctx.Cursors (F_Code_Zero).Last - Ctx.Cursors (F_Code_Zero).First + 1 = RFLX.ICMP.Code_Zero_Base'Size - and then Ctx.Cursors (F_Code_Zero).Predecessor = F_Tag - and then Ctx.Cursors (F_Code_Zero).First = Ctx.Cursors (F_Tag).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Checksum)) - then - Ctx.Cursors (F_Checksum).Last - Ctx.Cursors (F_Checksum).First + 1 = RFLX.ICMP.Checksum'Size - and then Ctx.Cursors (F_Checksum).Predecessor = F_Code_Zero - and then Ctx.Cursors (F_Checksum).First = Ctx.Cursors (F_Code_Zero).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Gateway_Internet_Address)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Redirect)) - then - Ctx.Cursors (F_Gateway_Internet_Address).Last - Ctx.Cursors (F_Gateway_Internet_Address).First + 1 = RFLX.ICMP.Gateway_Internet_Address'Size - and then Ctx.Cursors (F_Gateway_Internet_Address).Predecessor = F_Checksum - and then Ctx.Cursors (F_Gateway_Internet_Address).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Gateway_Internet_Address - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Gateway_Internet_Address).Last + 1)) - and then (if - Structural_Valid (Ctx.Cursors (F_Identifier)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Information_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply))) - then - Ctx.Cursors (F_Identifier).Last - Ctx.Cursors (F_Identifier).First + 1 = RFLX.ICMP.Identifier'Size - and then Ctx.Cursors (F_Identifier).Predecessor = F_Checksum - and then Ctx.Cursors (F_Identifier).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Sequence_Number)) - then - Ctx.Cursors (F_Sequence_Number).Last - Ctx.Cursors (F_Sequence_Number).First + 1 = RFLX.ICMP.Sequence_Number'Size - and then Ctx.Cursors (F_Sequence_Number).Predecessor = F_Identifier - and then Ctx.Cursors (F_Sequence_Number).First = Ctx.Cursors (F_Identifier).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Reply)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Echo_Request))) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = Ctx.Last - Ctx.Cursors (F_Sequence_Number).Last - and then Ctx.Cursors (F_Data).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Sequence_Number).Last + 1) - and then (if - Structural_Valid (Ctx.Cursors (F_Originate_Timestamp)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Msg)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Timestamp_Reply))) - then - Ctx.Cursors (F_Originate_Timestamp).Last - Ctx.Cursors (F_Originate_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Originate_Timestamp).Predecessor = F_Sequence_Number - and then Ctx.Cursors (F_Originate_Timestamp).First = Ctx.Cursors (F_Sequence_Number).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Receive_Timestamp)) - then - Ctx.Cursors (F_Receive_Timestamp).Last - Ctx.Cursors (F_Receive_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Receive_Timestamp).Predecessor = F_Originate_Timestamp - and then Ctx.Cursors (F_Receive_Timestamp).First = Ctx.Cursors (F_Originate_Timestamp).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Transmit_Timestamp)) - then - Ctx.Cursors (F_Transmit_Timestamp).Last - Ctx.Cursors (F_Transmit_Timestamp).First + 1 = RFLX.ICMP.Timestamp'Size - and then Ctx.Cursors (F_Transmit_Timestamp).Predecessor = F_Receive_Timestamp - and then Ctx.Cursors (F_Transmit_Timestamp).First = Ctx.Cursors (F_Receive_Timestamp).Last + 1))))) - and then (if - Structural_Valid (Ctx.Cursors (F_Pointer)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Parameter_Problem)) - then - Ctx.Cursors (F_Pointer).Last - Ctx.Cursors (F_Pointer).First + 1 = RFLX.ICMP.Pointer'Size - and then Ctx.Cursors (F_Pointer).Predecessor = F_Checksum - and then Ctx.Cursors (F_Pointer).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_24)) - then - Ctx.Cursors (F_Unused_24).Last - Ctx.Cursors (F_Unused_24).First + 1 = RFLX.ICMP.Unused_24_Base'Size - and then Ctx.Cursors (F_Unused_24).Predecessor = F_Pointer - and then Ctx.Cursors (F_Unused_24).First = Ctx.Cursors (F_Pointer).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_24 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_24).Last + 1))) - and then (if - Structural_Valid (Ctx.Cursors (F_Unused_32)) - and then (Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Time_Exceeded)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Destination_Unreachable)) - or Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Source_Quench))) - then - Ctx.Cursors (F_Unused_32).Last - Ctx.Cursors (F_Unused_32).First + 1 = RFLX.ICMP.Unused_32_Base'Size - and then Ctx.Cursors (F_Unused_32).Predecessor = F_Checksum - and then Ctx.Cursors (F_Unused_32).First = Ctx.Cursors (F_Checksum).Last + 1 - and then (if - Structural_Valid (Ctx.Cursors (F_Data)) - then - Ctx.Cursors (F_Data).Last - Ctx.Cursors (F_Data).First + 1 = 224 - and then Ctx.Cursors (F_Data).Predecessor = F_Unused_32 - and then Ctx.Cursors (F_Data).First = Ctx.Cursors (F_Unused_32).Last + 1)))))); - Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor); - Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data); - end Initialize_Bounded_Data; - end RFLX.ICMP.Generic_Message; diff --git a/tests/spark/generated/rflx-icmp-generic_message.ads b/tests/spark/generated/rflx-icmp-generic_message.ads index 6ef3be3012..d17f98f7cc 100644 --- a/tests/spark/generated/rflx-icmp-generic_message.ads +++ b/tests/spark/generated/rflx-icmp-generic_message.ads @@ -84,6 +84,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -129,10 +130,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -338,6 +336,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Tag) = Predecessor (Ctx, F_Tag)'Old and Valid_Next (Ctx, F_Tag) = Valid_Next (Ctx, F_Tag)'Old; @@ -373,6 +372,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Code_Destination_Unreachable) = Predecessor (Ctx, F_Code_Destination_Unreachable)'Old and Valid_Next (Ctx, F_Code_Destination_Unreachable) = Valid_Next (Ctx, F_Code_Destination_Unreachable)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -409,6 +409,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Code_Redirect) = Predecessor (Ctx, F_Code_Redirect)'Old and Valid_Next (Ctx, F_Code_Redirect) = Valid_Next (Ctx, F_Code_Redirect)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -445,6 +446,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Code_Time_Exceeded) = Predecessor (Ctx, F_Code_Time_Exceeded)'Old and Valid_Next (Ctx, F_Code_Time_Exceeded) = Valid_Next (Ctx, F_Code_Time_Exceeded)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -481,6 +483,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Code_Zero) = Predecessor (Ctx, F_Code_Zero)'Old and Valid_Next (Ctx, F_Code_Zero) = Valid_Next (Ctx, F_Code_Zero)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -542,6 +545,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Checksum) = Predecessor (Ctx, F_Checksum)'Old and Valid_Next (Ctx, F_Checksum) = Valid_Next (Ctx, F_Checksum)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -578,6 +582,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Gateway_Internet_Address) = Predecessor (Ctx, F_Gateway_Internet_Address)'Old and Valid_Next (Ctx, F_Gateway_Internet_Address) = Valid_Next (Ctx, F_Gateway_Internet_Address)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -615,6 +620,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Identifier) = Predecessor (Ctx, F_Identifier)'Old and Valid_Next (Ctx, F_Identifier) = Valid_Next (Ctx, F_Identifier)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -652,6 +658,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Pointer) = Predecessor (Ctx, F_Pointer)'Old and Valid_Next (Ctx, F_Pointer) = Valid_Next (Ctx, F_Pointer)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -689,6 +696,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Unused_32) = Predecessor (Ctx, F_Unused_32)'Old and Valid_Next (Ctx, F_Unused_32) = Valid_Next (Ctx, F_Unused_32)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -736,6 +744,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Sequence_Number) = Predecessor (Ctx, F_Sequence_Number)'Old and Valid_Next (Ctx, F_Sequence_Number) = Valid_Next (Ctx, F_Sequence_Number)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -774,6 +783,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Unused_24) = Predecessor (Ctx, F_Unused_24)'Old and Valid_Next (Ctx, F_Unused_24) = Valid_Next (Ctx, F_Unused_24)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -812,6 +822,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Originate_Timestamp) = Predecessor (Ctx, F_Originate_Timestamp)'Old and Valid_Next (Ctx, F_Originate_Timestamp) = Valid_Next (Ctx, F_Originate_Timestamp)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -850,6 +861,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Receive_Timestamp) = Predecessor (Ctx, F_Receive_Timestamp)'Old and Valid_Next (Ctx, F_Receive_Timestamp) = Valid_Next (Ctx, F_Receive_Timestamp)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -888,6 +900,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Transmit_Timestamp) = Predecessor (Ctx, F_Transmit_Timestamp)'Old and Valid_Next (Ctx, F_Transmit_Timestamp) = Valid_Next (Ctx, F_Transmit_Timestamp)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -930,6 +943,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -957,37 +971,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old - and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old - and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old - and Get_Tag (Ctx) = Get_Tag (Ctx)'Old - and Get_Checksum (Ctx) = Get_Checksum (Ctx)'Old - and Structural_Valid (Ctx, F_Data); - - generic - with procedure Process_Data (Data : out Types.Bytes); - with function Valid_Length (Length : Types.Length) return Boolean; - procedure Set_Bounded_Data (Ctx : in out Context; Size : Types.Bit_Length) with - Pre => - not Ctx'Constrained - and then Has_Buffer (Ctx) - and then Valid_Next (Ctx, F_Data) - and then Field_Last (Ctx, F_Data) <= Types.Bit_Index'Last / 2 - and then Field_Condition (Ctx, (Fld => F_Data)) - and then Available_Space (Ctx, F_Data) >= Size - and then Field_First (Ctx, F_Data) + Size <= Types.Bit_Index'Last / 2 - and then ((Valid (Ctx, F_Tag) - and (Get_Tag (Ctx) = Echo_Reply - or Get_Tag (Ctx) = Echo_Request))) - and then Field_First (Ctx, F_Data) mod Types.Byte'Size = 1 - and then Size mod Types.Byte'Size = 0 - and then Valid_Length (Types.Length (Size / Types.Byte'Size)), - Post => - Has_Buffer (Ctx) - and Invalid (Ctx, F_Receive_Timestamp) - and Invalid (Ctx, F_Transmit_Timestamp) - and Ctx.Buffer_First = Ctx.Buffer_First'Old - and Ctx.Buffer_Last = Ctx.Buffer_Last'Old - and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -1011,33 +995,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old - and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old - and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old - and Get_Tag (Ctx) = Get_Tag (Ctx)'Old - and Get_Checksum (Ctx) = Get_Checksum (Ctx)'Old - and Structural_Valid (Ctx, F_Data); - - procedure Initialize_Bounded_Data (Ctx : in out Context; Size : Types.Bit_Length) with - Pre => - not Ctx'Constrained - and then Has_Buffer (Ctx) - and then Valid_Next (Ctx, F_Data) - and then Field_Last (Ctx, F_Data) <= Types.Bit_Index'Last / 2 - and then Field_Condition (Ctx, (Fld => F_Data)) - and then Available_Space (Ctx, F_Data) >= Size - and then Field_First (Ctx, F_Data) + Size <= Types.Bit_Index'Last / 2 - and then ((Valid (Ctx, F_Tag) - and (Get_Tag (Ctx) = Echo_Reply - or Get_Tag (Ctx) = Echo_Request))) - and then Field_First (Ctx, F_Data) mod Types.Byte'Size = 1 - and then Size mod Types.Byte'Size = 0, - Post => - Has_Buffer (Ctx) - and Invalid (Ctx, F_Receive_Timestamp) - and Invalid (Ctx, F_Transmit_Timestamp) - and Ctx.Buffer_First = Ctx.Buffer_First'Old - and Ctx.Buffer_Last = Ctx.Buffer_Last'Old - and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -1127,7 +1085,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -1137,12 +1095,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -1764,11 +1724,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-ipv4-generic_option.adb b/tests/spark/generated/rflx-ipv4-generic_option.adb index db2d118bd2..bf300086b7 100644 --- a/tests/spark/generated/rflx-ipv4-generic_option.adb +++ b/tests/spark/generated/rflx-ipv4-generic_option.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Copied => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Copied => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Copied) - and then Available_Space (Ctx, F_Copied) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Copied) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Copied) and then Invalid (Ctx, F_Option_Class) and then Invalid (Ctx, F_Option_Number) @@ -36,18 +36,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Option_Data)) - then - Ctx.Cursors (F_Option_Data).Last - elsif - Structural_Valid (Ctx.Cursors (F_Option_Number)) - and then (Types.U64 (Ctx.Cursors (F_Option_Class).Value.Option_Class_Value) = Types.U64 (To_Base (Control)) - and Ctx.Cursors (F_Option_Number).Value.Option_Number_Value = 1) - then - Ctx.Cursors (F_Option_Number).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -298,7 +287,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -466,6 +455,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -650,7 +640,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -659,6 +649,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -698,7 +689,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Copied); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Copied) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Copied).Predecessor); Ctx.Cursors (Successor (Ctx, F_Copied)) := (State => S_Invalid, Predecessor => F_Copied); end Set_Copied; @@ -709,7 +700,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Option_Class); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Option_Class) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Option_Class).Predecessor); Ctx.Cursors (Successor (Ctx, F_Option_Class)) := (State => S_Invalid, Predecessor => F_Option_Class); end Set_Option_Class; @@ -720,7 +711,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Option_Number); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Option_Number) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Option_Number).Predecessor); Ctx.Cursors (Successor (Ctx, F_Option_Number)) := (State => S_Invalid, Predecessor => F_Option_Number); end Set_Option_Number; @@ -731,7 +722,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Option_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Option_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Option_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Option_Length)) := (State => S_Invalid, Predecessor => F_Option_Length); end Set_Option_Length; @@ -741,7 +732,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Option_Data); begin Reset_Dependent_Fields (Ctx, F_Option_Data); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Option_Data) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Option_Data), Predecessor => Ctx.Cursors (F_Option_Data).Predecessor); Ctx.Cursors (Successor (Ctx, F_Option_Data)) := (State => S_Invalid, Predecessor => F_Option_Data); end Set_Option_Data_Empty; @@ -763,7 +754,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Option_Data); begin Reset_Dependent_Fields (Ctx, F_Option_Data); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Copied)) then diff --git a/tests/spark/generated/rflx-ipv4-generic_option.ads b/tests/spark/generated/rflx-ipv4-generic_option.ads index 98dae8a6c3..7138dd8a93 100644 --- a/tests/spark/generated/rflx-ipv4-generic_option.ads +++ b/tests/spark/generated/rflx-ipv4-generic_option.ads @@ -65,6 +65,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -110,10 +111,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -239,6 +237,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Copied) = Predecessor (Ctx, F_Copied)'Old and Valid_Next (Ctx, F_Copied) = Valid_Next (Ctx, F_Copied)'Old; @@ -263,6 +262,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Class) = Predecessor (Ctx, F_Option_Class)'Old and Valid_Next (Ctx, F_Option_Class) = Valid_Next (Ctx, F_Option_Class)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -291,6 +291,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Number) = Predecessor (Ctx, F_Option_Number)'Old and Valid_Next (Ctx, F_Option_Number) = Valid_Next (Ctx, F_Option_Number)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -331,6 +332,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Length) = Predecessor (Ctx, F_Option_Length)'Old and Valid_Next (Ctx, F_Option_Length) = Valid_Next (Ctx, F_Option_Length)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -356,6 +358,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Data) = Predecessor (Ctx, F_Option_Data)'Old and Valid_Next (Ctx, F_Option_Data) = Valid_Next (Ctx, F_Option_Data)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -383,6 +386,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Data) = Predecessor (Ctx, F_Option_Data)'Old and Valid_Next (Ctx, F_Option_Data) = Valid_Next (Ctx, F_Option_Data)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -406,6 +410,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Option_Data) = Predecessor (Ctx, F_Option_Data)'Old and Valid_Next (Ctx, F_Option_Data) = Valid_Next (Ctx, F_Option_Data)'Old and Get_Copied (Ctx) = Get_Copied (Ctx)'Old @@ -475,7 +480,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -485,12 +490,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -588,11 +595,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-ipv4-generic_packet.adb b/tests/spark/generated/rflx-ipv4-generic_packet.adb index a7231763b7..226508896a 100644 --- a/tests/spark/generated/rflx-ipv4-generic_packet.adb +++ b/tests/spark/generated/rflx-ipv4-generic_packet.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Version => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Version => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Version) - and then Available_Space (Ctx, F_Version) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Version) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Version) and then Invalid (Ctx, F_IHL) and then Invalid (Ctx, F_DSCP) @@ -48,12 +48,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Payload)) - then - Ctx.Cursors (F_Payload).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -565,7 +560,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -1215,6 +1210,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -1546,7 +1542,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -1555,6 +1551,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -1624,7 +1621,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Version); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Version) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Version).Predecessor); Ctx.Cursors (Successor (Ctx, F_Version)) := (State => S_Invalid, Predecessor => F_Version); end Set_Version; @@ -1635,7 +1632,7 @@ is begin Reset_Dependent_Fields (Ctx, F_IHL); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_IHL) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_IHL).Predecessor); Ctx.Cursors (Successor (Ctx, F_IHL)) := (State => S_Invalid, Predecessor => F_IHL); end Set_IHL; @@ -1646,7 +1643,7 @@ is begin Reset_Dependent_Fields (Ctx, F_DSCP); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_DSCP) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_DSCP).Predecessor); Ctx.Cursors (Successor (Ctx, F_DSCP)) := (State => S_Invalid, Predecessor => F_DSCP); end Set_DSCP; @@ -1657,7 +1654,7 @@ is begin Reset_Dependent_Fields (Ctx, F_ECN); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_ECN) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_ECN).Predecessor); Ctx.Cursors (Successor (Ctx, F_ECN)) := (State => S_Invalid, Predecessor => F_ECN); end Set_ECN; @@ -1668,7 +1665,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Total_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Total_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Total_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Total_Length)) := (State => S_Invalid, Predecessor => F_Total_Length); end Set_Total_Length; @@ -1679,7 +1676,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Identification); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Identification) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Identification).Predecessor); Ctx.Cursors (Successor (Ctx, F_Identification)) := (State => S_Invalid, Predecessor => F_Identification); end Set_Identification; @@ -1690,7 +1687,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Flag_R); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Flag_R) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Flag_R).Predecessor); Ctx.Cursors (Successor (Ctx, F_Flag_R)) := (State => S_Invalid, Predecessor => F_Flag_R); end Set_Flag_R; @@ -1701,7 +1698,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Flag_DF); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Flag_DF) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Flag_DF).Predecessor); Ctx.Cursors (Successor (Ctx, F_Flag_DF)) := (State => S_Invalid, Predecessor => F_Flag_DF); end Set_Flag_DF; @@ -1712,7 +1709,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Flag_MF); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Flag_MF) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Flag_MF).Predecessor); Ctx.Cursors (Successor (Ctx, F_Flag_MF)) := (State => S_Invalid, Predecessor => F_Flag_MF); end Set_Flag_MF; @@ -1723,7 +1720,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Fragment_Offset); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Fragment_Offset) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Fragment_Offset).Predecessor); Ctx.Cursors (Successor (Ctx, F_Fragment_Offset)) := (State => S_Invalid, Predecessor => F_Fragment_Offset); end Set_Fragment_Offset; @@ -1734,7 +1731,7 @@ is begin Reset_Dependent_Fields (Ctx, F_TTL); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_TTL) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_TTL).Predecessor); Ctx.Cursors (Successor (Ctx, F_TTL)) := (State => S_Invalid, Predecessor => F_TTL); end Set_TTL; @@ -1745,7 +1742,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Protocol); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Protocol) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Protocol).Predecessor); Ctx.Cursors (Successor (Ctx, F_Protocol)) := (State => S_Invalid, Predecessor => F_Protocol); end Set_Protocol; @@ -1756,7 +1753,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Header_Checksum); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Header_Checksum) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Header_Checksum).Predecessor); Ctx.Cursors (Successor (Ctx, F_Header_Checksum)) := (State => S_Invalid, Predecessor => F_Header_Checksum); end Set_Header_Checksum; @@ -1767,7 +1764,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Source); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Source) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Source).Predecessor); Ctx.Cursors (Successor (Ctx, F_Source)) := (State => S_Invalid, Predecessor => F_Source); end Set_Source; @@ -1778,7 +1775,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Destination); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Destination) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Destination).Predecessor); Ctx.Cursors (Successor (Ctx, F_Destination)) := (State => S_Invalid, Predecessor => F_Destination); end Set_Destination; @@ -1788,7 +1785,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Options); begin Reset_Dependent_Fields (Ctx, F_Options); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Options) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Options), Predecessor => Ctx.Cursors (F_Options).Predecessor); Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, Predecessor => F_Options); end Set_Options_Empty; @@ -1798,7 +1795,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Payload) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Payload), Predecessor => Ctx.Cursors (F_Payload).Predecessor); Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload); end Set_Payload_Empty; @@ -1820,7 +1817,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Version)) then @@ -1936,7 +1933,7 @@ is begin if Invalid (Ctx, F_Options) then Reset_Dependent_Fields (Ctx, F_Options); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Version)) then diff --git a/tests/spark/generated/rflx-ipv4-generic_packet.ads b/tests/spark/generated/rflx-ipv4-generic_packet.ads index b6527389ef..b6f07db494 100644 --- a/tests/spark/generated/rflx-ipv4-generic_packet.ads +++ b/tests/spark/generated/rflx-ipv4-generic_packet.ads @@ -89,6 +89,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -134,10 +135,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -326,6 +324,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Version) = Predecessor (Ctx, F_Version)'Old and Valid_Next (Ctx, F_Version) = Valid_Next (Ctx, F_Version)'Old; @@ -362,6 +361,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_IHL) = Predecessor (Ctx, F_IHL)'Old and Valid_Next (Ctx, F_IHL) = Valid_Next (Ctx, F_IHL)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -399,6 +399,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_DSCP) = Predecessor (Ctx, F_DSCP)'Old and Valid_Next (Ctx, F_DSCP) = Valid_Next (Ctx, F_DSCP)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -437,6 +438,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_ECN) = Predecessor (Ctx, F_ECN)'Old and Valid_Next (Ctx, F_ECN) = Valid_Next (Ctx, F_ECN)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -479,6 +481,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Total_Length) = Predecessor (Ctx, F_Total_Length)'Old and Valid_Next (Ctx, F_Total_Length) = Valid_Next (Ctx, F_Total_Length)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -519,6 +522,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Identification) = Predecessor (Ctx, F_Identification)'Old and Valid_Next (Ctx, F_Identification) = Valid_Next (Ctx, F_Identification)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -563,6 +567,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Flag_R) = Predecessor (Ctx, F_Flag_R)'Old and Valid_Next (Ctx, F_Flag_R) = Valid_Next (Ctx, F_Flag_R)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -605,6 +610,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Flag_DF) = Predecessor (Ctx, F_Flag_DF)'Old and Valid_Next (Ctx, F_Flag_DF) = Valid_Next (Ctx, F_Flag_DF)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -648,6 +654,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Flag_MF) = Predecessor (Ctx, F_Flag_MF)'Old and Valid_Next (Ctx, F_Flag_MF) = Valid_Next (Ctx, F_Flag_MF)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -692,6 +699,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Fragment_Offset) = Predecessor (Ctx, F_Fragment_Offset)'Old and Valid_Next (Ctx, F_Fragment_Offset) = Valid_Next (Ctx, F_Fragment_Offset)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -737,6 +745,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_TTL) = Predecessor (Ctx, F_TTL)'Old and Valid_Next (Ctx, F_TTL) = Valid_Next (Ctx, F_TTL)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -783,6 +792,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Protocol) = Predecessor (Ctx, F_Protocol)'Old and Valid_Next (Ctx, F_Protocol) = Valid_Next (Ctx, F_Protocol)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -830,6 +840,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Header_Checksum) = Predecessor (Ctx, F_Header_Checksum)'Old and Valid_Next (Ctx, F_Header_Checksum) = Valid_Next (Ctx, F_Header_Checksum)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -878,6 +889,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Source) = Predecessor (Ctx, F_Source)'Old and Valid_Next (Ctx, F_Source) = Valid_Next (Ctx, F_Source)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -927,6 +939,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Destination) = Predecessor (Ctx, F_Destination)'Old and Valid_Next (Ctx, F_Destination) = Valid_Next (Ctx, F_Destination)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -977,6 +990,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Options) = Predecessor (Ctx, F_Options)'Old and Valid_Next (Ctx, F_Options) = Valid_Next (Ctx, F_Options)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -1012,6 +1026,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -1050,6 +1065,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -1084,6 +1100,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Version (Ctx) = Get_Version (Ctx)'Old @@ -1273,7 +1290,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -1283,12 +1300,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -1544,11 +1563,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-tlv-generic_message.adb b/tests/spark/generated/rflx-tlv-generic_message.adb index b3d6601df0..6caa218876 100644 --- a/tests/spark/generated/rflx-tlv-generic_message.adb +++ b/tests/spark/generated/rflx-tlv-generic_message.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Tag => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Tag => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Tag) - and then Available_Space (Ctx, F_Tag) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Tag) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Tag) and then Invalid (Ctx, F_Length) and then Invalid (Ctx, F_Value)); @@ -34,17 +34,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Tag)) - and then Types.U64 (Ctx.Cursors (F_Tag).Value.Tag_Value) = Types.U64 (To_Base (Msg_Error)) - then - Ctx.Cursors (F_Tag).Last - elsif - Structural_Valid (Ctx.Cursors (F_Value)) - then - Ctx.Cursors (F_Value).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -189,7 +179,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -318,6 +308,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -434,7 +425,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -443,6 +434,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -476,7 +468,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Tag); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Tag) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Tag).Predecessor); Ctx.Cursors (Successor (Ctx, F_Tag)) := (State => S_Invalid, Predecessor => F_Tag); end Set_Tag; @@ -487,7 +479,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length); end Set_Length; @@ -497,7 +489,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Value); begin Reset_Dependent_Fields (Ctx, F_Value); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Value) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Value), Predecessor => Ctx.Cursors (F_Value).Predecessor); Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, Predecessor => F_Value); end Set_Value_Empty; @@ -519,7 +511,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Value); begin Reset_Dependent_Fields (Ctx, F_Value); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Tag)) then diff --git a/tests/spark/generated/rflx-tlv-generic_message.ads b/tests/spark/generated/rflx-tlv-generic_message.ads index 12de11bfcb..9b06e12d92 100644 --- a/tests/spark/generated/rflx-tlv-generic_message.ads +++ b/tests/spark/generated/rflx-tlv-generic_message.ads @@ -58,6 +58,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -103,10 +104,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -225,6 +223,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Tag) = Predecessor (Ctx, F_Tag)'Old and Valid_Next (Ctx, F_Tag) = Valid_Next (Ctx, F_Tag)'Old; @@ -247,6 +246,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -268,6 +268,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Value) = Predecessor (Ctx, F_Value)'Old and Valid_Next (Ctx, F_Value) = Valid_Next (Ctx, F_Value)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -293,6 +294,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Value) = Predecessor (Ctx, F_Value)'Old and Valid_Next (Ctx, F_Value) = Valid_Next (Ctx, F_Value)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -314,6 +316,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Value) = Predecessor (Ctx, F_Value)'Old and Valid_Next (Ctx, F_Value) = Valid_Next (Ctx, F_Value)'Old and Get_Tag (Ctx) = Get_Tag (Ctx)'Old @@ -377,7 +380,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -387,12 +390,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -436,11 +441,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/generated/rflx-udp-generic_datagram.adb b/tests/spark/generated/rflx-udp-generic_datagram.adb index 60bd03d67b..e4e0040098 100644 --- a/tests/spark/generated/rflx-udp-generic_datagram.adb +++ b/tests/spark/generated/rflx-udp-generic_datagram.adb @@ -13,13 +13,13 @@ is Buffer_First : constant Types.Index := Buffer'First; Buffer_Last : constant Types.Index := Buffer'Last; begin - Ctx := (Buffer_First, Buffer_Last, First, Last, Buffer, (F_Source_Port => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); + Ctx := (Buffer_First, Buffer_Last, First, Last, First, Buffer, (F_Source_Port => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final))); Buffer := null; end Initialize; function Initialized (Ctx : Context) return Boolean is (Valid_Next (Ctx, F_Source_Port) - and then Available_Space (Ctx, F_Source_Port) = Types.Last_Bit_Index (Ctx.Buffer_Last) - Ctx.First + 1 + and then Available_Space (Ctx, F_Source_Port) = Ctx.Last - Ctx.First + 1 and then Invalid (Ctx, F_Source_Port) and then Invalid (Ctx, F_Destination_Port) and then Invalid (Ctx, F_Length) @@ -36,12 +36,7 @@ is (Ctx.Buffer /= null); function Message_Last (Ctx : Context) return Types.Bit_Index is - ((if - Structural_Valid (Ctx.Cursors (F_Payload)) - then - Ctx.Cursors (F_Payload).Last - else - Types.Unreachable_Bit_Length)); + (Ctx.Message_Last); function Path_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Ctx.Cursors (Fld).Predecessor is @@ -221,7 +216,7 @@ is and then Path_Condition (Ctx, Fld)); function Available_Space (Ctx : Context; Fld : Field) return Types.Bit_Length is - (Types.Last_Bit_Index (Ctx.Buffer_Last) - Field_First (Ctx, Fld) + 1); + (Ctx.Last - Field_First (Ctx, Fld) + 1); function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is (Ctx.Buffer /= null @@ -388,6 +383,7 @@ is Valid_Value (Value) and Field_Condition (Ctx, Value) then + Ctx.Message_Last := Field_Last (Ctx, Fld); 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); else @@ -529,7 +525,7 @@ is and Lst = Field_Last (Ctx, Val.Fld) and Fst >= Ctx.First and Fst <= Lst + 1 - and Types.Byte_Index (Lst) <= Ctx.Buffer_Last + and Lst <= Ctx.Last and (for all F in Field'Range => (if Structural_Valid (Ctx.Cursors (F)) @@ -538,6 +534,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Ctx.Cursors = Ctx.Cursors'Old is First : constant Types.Bit_Index := Field_First (Ctx, Val.Fld); @@ -576,7 +573,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Source_Port); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Source_Port) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Source_Port).Predecessor); Ctx.Cursors (Successor (Ctx, F_Source_Port)) := (State => S_Invalid, Predecessor => F_Source_Port); end Set_Source_Port; @@ -587,7 +584,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Destination_Port); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Destination_Port) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Destination_Port).Predecessor); Ctx.Cursors (Successor (Ctx, F_Destination_Port)) := (State => S_Invalid, Predecessor => F_Destination_Port); end Set_Destination_Port; @@ -598,7 +595,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Length); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor); Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length); end Set_Length; @@ -609,7 +606,7 @@ is begin Reset_Dependent_Fields (Ctx, F_Checksum); Set_Field_Value (Ctx, Field_Value, First, Last); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Checksum) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Checksum).Predecessor); Ctx.Cursors (Successor (Ctx, F_Checksum)) := (State => S_Invalid, Predecessor => F_Checksum); end Set_Checksum; @@ -619,7 +616,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; Ctx.Cursors (F_Payload) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Payload), Predecessor => Ctx.Cursors (F_Payload).Predecessor); Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload); end Set_Payload_Empty; @@ -641,7 +638,7 @@ is Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload); begin Reset_Dependent_Fields (Ctx, F_Payload); - Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors); + Ctx.Message_Last := Last; pragma Assert ((if Structural_Valid (Ctx.Cursors (F_Source_Port)) then diff --git a/tests/spark/generated/rflx-udp-generic_datagram.ads b/tests/spark/generated/rflx-udp-generic_datagram.ads index 05fb51053c..de8eab9e7b 100644 --- a/tests/spark/generated/rflx-udp-generic_datagram.ads +++ b/tests/spark/generated/rflx-udp-generic_datagram.ads @@ -62,6 +62,7 @@ is and Ctx.Buffer_First = Buffer'First'Old and Ctx.Buffer_Last = Buffer'Last'Old and Ctx.First = Types.First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = Types.Last_Bit_Index (Ctx.Buffer_Last) and Initialized (Ctx), Depends => (Ctx => Buffer, Buffer => null); @@ -107,10 +108,7 @@ is function Has_Buffer (Ctx : Context) return Boolean; - function Message_Last (Ctx : Context) return Types.Bit_Index with - Pre => - Has_Buffer (Ctx) - and then Structural_Valid_Message (Ctx); + function Message_Last (Ctx : Context) return Types.Bit_Index; function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => @@ -236,6 +234,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Source_Port) = Predecessor (Ctx, F_Source_Port)'Old and Valid_Next (Ctx, F_Source_Port) = Valid_Next (Ctx, F_Source_Port)'Old; @@ -260,6 +259,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Destination_Port) = Predecessor (Ctx, F_Destination_Port)'Old and Valid_Next (Ctx, F_Destination_Port) = Valid_Next (Ctx, F_Destination_Port)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -285,6 +285,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -311,6 +312,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Checksum) = Predecessor (Ctx, F_Checksum)'Old and Valid_Next (Ctx, F_Checksum) = Valid_Next (Ctx, F_Checksum)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -336,6 +338,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -363,6 +366,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -386,6 +390,7 @@ is and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old and Get_Source_Port (Ctx) = Get_Source_Port (Ctx)'Old @@ -455,7 +460,7 @@ private (Cursor.State = S_Invalid or Cursor.State = S_Incomplete); - function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is + function Valid_Context (Buffer_First, Buffer_Last : Types.Index; First, Last, Message_Last : Types.Bit_Index; Buffer : access constant Types.Bytes; Cursors : Field_Cursors) return Boolean is ((if Buffer /= null then @@ -465,12 +470,14 @@ private and Types.Byte_Index (Last) <= Buffer_Last and First <= Last and Last <= Types.Bit_Index'Last / 2) + and then First <= Message_Last + and then Message_Last <= Last and then (for all F in Field'First .. Field'Last => (if Structural_Valid (Cursors (F)) then Cursors (F).First >= First - and Cursors (F).Last <= Last + and Cursors (F).Last <= Message_Last and Cursors (F).First <= Cursors (F).Last + 1 and Cursors (F).Value.Fld = F)) and then ((if @@ -542,11 +549,12 @@ private type Context (Buffer_First, Buffer_Last : Types.Index := Types.Index'First; First, Last : Types.Bit_Index := Types.Bit_Index'First) is record + Message_Last : Types.Bit_Index := First; Buffer : Types.Bytes_Ptr := null; Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final)); end record with Dynamic_Predicate => - Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Buffer, Context.Cursors); + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors); function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is (Ctx.Cursors (Fld)); diff --git a/tests/spark/rflx-arrays-tests.adb b/tests/spark/rflx-arrays-tests.adb index 19b9f93dd7..728d4e135a 100644 --- a/tests/spark/rflx-arrays-tests.adb +++ b/tests/spark/rflx-arrays-tests.adb @@ -12,6 +12,7 @@ with RFLX.Arrays.AV_Enumeration_Vector; with RFLX.Arrays.Messages_Message; with RFLX.Arrays.Inner_Message; with RFLX.Arrays.Inner_Messages; +with RFLX.Arrays.Array_Size_Defined_By_Message_Size; package body RFLX.Arrays.Tests is @@ -1061,6 +1062,108 @@ package body RFLX.Arrays.Tests is Assert (Sequence_Context.Last'Image, RFLX_Builtin_Types.Bit_Length (48)'Image, "Invalid Sequence_Context.Last"); end Test_Generating_Arrays_Messages_Message; + procedure Test_Parsing_Array_Size_Defined_By_Message_Size (T : in out AUnit.Test_Cases.Test_Case'Class) with + SPARK_Mode, Pre => True + is + pragma Unreferenced (T); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 1, 0, 2); + Context : Arrays.Array_Size_Defined_By_Message_Size.Context; + Sequence_Context : Arrays.Modular_Vector.Context; + Header : Arrays.Enumeration; + Element : Arrays.Modular_Integer; + I : Natural := 1; + package Message renames Arrays.Array_Size_Defined_By_Message_Size; + begin + Message.Initialize (Context, Buffer); + + Message.Verify_Message (Context); + + if Message.Valid (Context, Message.F_Header) then + Header := Message.Get_Header (Context); + + Assert (Header'Image, Arrays.ONE'Image, "Invalid value of Header"); + + if Message.Present (Context, Message.F_Vector) then + Message.Switch_To_Vector (Context, Sequence_Context); + + while I <= 10 and then Arrays.Modular_Vector.Valid_Element (Sequence_Context) loop + pragma Loop_Invariant (Arrays.Modular_Vector.Has_Buffer (Sequence_Context)); + pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First); + pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last); + pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry); + pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry); + + Element := Arrays.Modular_Vector.Get_Element (Sequence_Context); + + Assert (Element'Image, Natural'Image (I), "Invalid value of element " & I'Image); + + Arrays.Modular_Vector.Next (Sequence_Context); + I := I + 1; + end loop; + + Assert (I'Image, Natural'Image (3), "Unexpected number of elements"); + Assert (Arrays.Modular_Vector.Valid (Sequence_Context), "Invalid Vector after parsing"); + Assert (not Message.Valid (Context, Message.F_Vector), + "Valid Vector before context update"); + + Message.Update_Vector (Context, Sequence_Context); + + Assert (Message.Valid (Context, Message.F_Vector), + "Invalid Vector after context update"); + else + Assert (False, "Invalid Vector or Buffer"); + end if; + end if; + + Assert (Message.Valid_Message (Context), "Invalid Message"); + + if Message.Has_Buffer (Context) then + Message.Take_Buffer (Context, Buffer); + end if; + Free_Bytes_Ptr (Buffer); + + Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (40)'Image, "Invalid Context.Last"); + Assert (Sequence_Context.Last'Image, RFLX_Builtin_Types.Bit_Length (40)'Image, "Invalid Sequence_Context.Last"); + end Test_Parsing_Array_Size_Defined_By_Message_Size; + + procedure Test_Generating_Array_Size_Defined_By_Message_Size (T : in out AUnit.Test_Cases.Test_Case'Class) with + SPARK_Mode, Pre => True + is + pragma Unreferenced (T); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0); + Context : Arrays.Array_Size_Defined_By_Message_Size.Context; + Sequence_Context : Arrays.Modular_Vector.Context; + package Message renames Arrays.Array_Size_Defined_By_Message_Size; + begin + Message.Initialize (Context, Buffer); + + Message.Set_Header (Context, Arrays.ONE); + Message.Switch_To_Vector (Context, Sequence_Context); + Arrays.Modular_Vector.Append_Element (Sequence_Context, 1); + Arrays.Modular_Vector.Append_Element (Sequence_Context, 2); + + Assert (not Arrays.Modular_Vector.Valid_Element (Sequence_Context), + "Invalid acceptance of further element"); + Assert (not Message.Valid (Context, Message.F_Vector), + "Valid Modular_Vector before context update"); + Assert (not Message.Valid (Context, Message.F_Vector), + "Valid Modular_Vector before context update"); + + Message.Update_Vector (Context, Sequence_Context); + + Assert (Message.Valid (Context, Message.F_Vector), + "Invalid Modular_Vector after context update"); + Assert (Message.Valid_Message (Context), "Invalid Message"); + + if Message.Has_Buffer (Context) then + Message.Take_Buffer (Context, Buffer); + end if; + Free_Bytes_Ptr (Buffer); + + Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (40)'Image, "Invalid Context.Last"); + Assert (Sequence_Context.Last'Image, RFLX_Builtin_Types.Bit_Length (40)'Image, "Invalid Sequence_Context.Last"); + end Test_Generating_Array_Size_Defined_By_Message_Size; + overriding procedure Register_Tests (T : in out Test) is use AUnit.Test_Cases.Registration; @@ -1079,6 +1182,10 @@ package body RFLX.Arrays.Tests is Register_Routine (T, Test_Parsing_Arrays_Messages_Message_Loop'Access, "Parsing Messages Message Loop"); Register_Routine (T, Test_Generating_Arrays_Message'Access, "Generating Message"); Register_Routine (T, Test_Generating_Arrays_Messages_Message'Access, "Generating Messages Message"); + Register_Routine (T, Test_Parsing_Array_Size_Defined_By_Message_Size'Access, + "Parsing message with array size defined by message size"); + Register_Routine (T, Test_Generating_Array_Size_Defined_By_Message_Size'Access, + "Generating message with array size defined by message size"); end Register_Tests; end RFLX.Arrays.Tests; diff --git a/tests/spark/rflx-enumeration-tests.adb b/tests/spark/rflx-enumeration-tests.adb index 9e05c27c5d..462cf81af2 100644 --- a/tests/spark/rflx-enumeration-tests.adb +++ b/tests/spark/rflx-enumeration-tests.adb @@ -92,11 +92,13 @@ package body RFLX.Enumeration.Tests is Enumeration.Message.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Enumeration.Message.Message_Last (Context)) - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (Enumeration.Message.Message_Last (Context))), Expected.all, "Invalid binary representation"); diff --git a/tests/spark/rflx-ethernet-tests.adb b/tests/spark/rflx-ethernet-tests.adb index eeed426606..7503e6fcaa 100644 --- a/tests/spark/rflx-ethernet-tests.adb +++ b/tests/spark/rflx-ethernet-tests.adb @@ -313,20 +313,20 @@ package body RFLX.Ethernet.Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - procedure Set_Bounded_Payload is new Ethernet.Frame.Set_Bounded_Payload (Write_Data, Valid_Data_Length); + procedure Set_Payload is new Ethernet.Frame.Set_Payload (Write_Data, Valid_Data_Length); Expected : RFLX_Builtin_Types.Bytes_Ptr := Read_File_Ptr ("tests/data/captured/ethernet_ipv4_udp.raw"); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First .. RFLX_Builtin_Types.Index'First + 2000 - 1 => 0); Context : Ethernet.Frame.Context; begin - Ethernet.Frame.Initialize (Context, Buffer, 801, 801); + Ethernet.Frame.Initialize (Context, Buffer, 801, 1280); Ethernet.Frame.Set_Destination (Context, 16#FFFFFFFFFFFF#); Ethernet.Frame.Set_Source (Context, 16#000000000000#); Ethernet.Frame.Set_Type_Length_TPID (Context, 16#0800#); Ethernet.Frame.Set_Type_Length (Context, 16#0800#); Data := (69, 0, 0, 46, 0, 1, 0, 0, 64, 17, 124, 188, 127, 0, 0, 1, 127, 0, 0, 1, 0, 53, 0, 53, 0, 26, 1, 78, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0); - Set_Bounded_Payload (Context, 46 * 8); + Set_Payload (Context); Assert (Ethernet.Frame.Structural_Valid_Message (Context), "Structural invalid frame"); Assert (not Ethernet.Frame.Valid_Message (Context), "Valid frame"); @@ -367,10 +367,13 @@ package body RFLX.Ethernet.Tests is Ethernet.Frame.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context)) - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), Expected.all, + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context))), + Expected.all, "Invalid binary representation"); Free_Bytes_Ptr (Expected); @@ -381,13 +384,13 @@ package body RFLX.Ethernet.Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - procedure Set_Bounded_Payload is new Ethernet.Frame.Set_Bounded_Payload (Write_Data, Valid_Data_Length); + procedure Set_Payload is new Ethernet.Frame.Set_Payload (Write_Data, Valid_Data_Length); Expected : RFLX_Builtin_Types.Bytes_Ptr := Read_File_Ptr ("tests/data/captured/ethernet_vlan_tag.raw"); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First .. RFLX_Builtin_Types.Index'First + 2000 - 1 => 0); Context : Ethernet.Frame.Context; begin - Ethernet.Frame.Initialize (Context, Buffer, 801, 801); + Ethernet.Frame.Initialize (Context, Buffer, 801, 1320); Ethernet.Frame.Set_Destination (Context, 16#FFFFFFFFFFFF#); Ethernet.Frame.Set_Source (Context, 16#000000000000#); Ethernet.Frame.Set_Type_Length_TPID (Context, 16#8100#); @@ -396,16 +399,19 @@ package body RFLX.Ethernet.Tests is Ethernet.Frame.Set_Type_Length (Context, 16#0800#); Data := (69, 0, 0, 47, 0, 1, 0, 0, 64, 0, 124, 231, 127, 0, 0, 1, 127, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10); - Set_Bounded_Payload (Context, 47 * 8); + Set_Payload (Context); Assert (Ethernet.Frame.Structural_Valid_Message (Context), "Structural invalid frame"); Assert (not Ethernet.Frame.Valid_Message (Context), "Valid frame"); Ethernet.Frame.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context)) - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), Expected.all, + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context))), + Expected.all, "Invalid binary representation"); Free_Bytes_Ptr (Expected); @@ -427,13 +433,13 @@ package body RFLX.Ethernet.Tests is -- Simulate a type/length/TPID value that is determined at runtime function Dynamic_Type_Length is new Identity (Ethernet.Type_Length); - procedure Set_Bounded_Payload is new Ethernet.Frame.Set_Bounded_Payload (Write_Data, Valid_Data_Length); + procedure Set_Payload is new Ethernet.Frame.Set_Payload (Write_Data, Valid_Data_Length); Expected : RFLX_Builtin_Types.Bytes_Ptr := Read_File_Ptr ("tests/data/captured/ethernet_vlan_tag.raw"); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First .. RFLX_Builtin_Types.Index'First + 2000 - 1 => 0); Context : Ethernet.Frame.Context; begin - Ethernet.Frame.Initialize (Context, Buffer, 801, 801); + Ethernet.Frame.Initialize (Context, Buffer, 801, 1320); Ethernet.Frame.Set_Destination (Context, 16#FFFFFFFFFFFF#); Ethernet.Frame.Set_Source (Context, 16#000000000000#); Ethernet.Frame.Set_Type_Length_TPID (Context, Dynamic_Type_Length (16#8100#)); @@ -443,7 +449,7 @@ package body RFLX.Ethernet.Tests is Ethernet.Frame.Set_Type_Length (Context, 16#0800#); Data := (69, 0, 0, 47, 0, 1, 0, 0, 64, 0, 124, 231, 127, 0, 0, 1, 127, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10); - Set_Bounded_Payload (Context, 47 * 8); + Set_Payload (Context); end if; Assert (Ethernet.Frame.Structural_Valid_Message (Context), "Structural invalid frame"); @@ -451,10 +457,13 @@ package body RFLX.Ethernet.Tests is Ethernet.Frame.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context)) - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), Expected.all, + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Context))), + Expected.all, "Invalid binary representation"); Free_Bytes_Ptr (Expected); diff --git a/tests/spark/rflx-in_ethernet-tests.adb b/tests/spark/rflx-in_ethernet-tests.adb index 73bdc930bf..a4da0732f3 100644 --- a/tests/spark/rflx-in_ethernet-tests.adb +++ b/tests/spark/rflx-in_ethernet-tests.adb @@ -79,7 +79,7 @@ package body RFLX.In_Ethernet.Tests is Read_File_Ptr ("tests/data/captured/ethernet_ipv4_udp.raw"); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First - .. RFLX_Builtin_Types.Index'First + Expected'Size - 1 => 0); + .. RFLX_Builtin_Types.Index'First + Expected'Length - 1 => 0); Ethernet_Frame_Context : Ethernet.Frame.Context; IPv4_Packet_Context : IPv4.Packet.Context; begin @@ -88,7 +88,7 @@ package body RFLX.In_Ethernet.Tests is Ethernet.Frame.Set_Source (Ethernet_Frame_Context, 16#000000000000#); Ethernet.Frame.Set_Type_Length_TPID (Ethernet_Frame_Context, 16#0800#); Ethernet.Frame.Set_Type_Length (Ethernet_Frame_Context, 16#0800#); - Ethernet.Frame.Initialize_Bounded_Payload (Ethernet_Frame_Context, 368); + Ethernet.Frame.Initialize_Payload (Ethernet_Frame_Context); Assert (Ethernet.Frame.Structural_Valid_Message (Ethernet_Frame_Context), "Structural invalid frame"); Assert (not Ethernet.Frame.Valid_Message (Ethernet_Frame_Context), "Valid frame"); @@ -120,11 +120,11 @@ package body RFLX.In_Ethernet.Tests is IPv4.Packet.Take_Buffer (IPv4_Packet_Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (IPv4_Packet_Context.Last) + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (IPv4.Packet.Message_Last (IPv4_Packet_Context)) - RFLX_Types.Byte_Index (Ethernet_Frame_Context.First) + 1), Expected'Length'Img, "Invalid buffer length"); Assert (Buffer.all (RFLX_Types.Byte_Index (Ethernet_Frame_Context.First) - .. RFLX_Types.Byte_Index (Ethernet_Frame_Context.Last)), Expected.all, + .. RFLX_Types.Byte_Index (Ethernet.Frame.Message_Last (Ethernet_Frame_Context))), Expected.all, "Invalid binary representation"); end if; diff --git a/tests/spark/rflx-in_ipv4-tests.adb b/tests/spark/rflx-in_ipv4-tests.adb index b0cfabfbcd..490c758b15 100644 --- a/tests/spark/rflx-in_ipv4-tests.adb +++ b/tests/spark/rflx-in_ipv4-tests.adb @@ -133,7 +133,7 @@ package body RFLX.In_IPv4.Tests is Read_File_Ptr ("tests/data/captured/ethernet_ipv4_udp.raw"); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First - .. RFLX_Builtin_Types.Index'First + Expected'Size - 1 => 0); + .. RFLX_Builtin_Types.Index'First + Expected'Length - 1 => 0); Ethernet_Frame_Context : Ethernet.Frame.Context; IPv4_Packet_Context : IPv4.Packet.Context; UDP_Datagram_Context : UDP.Datagram.Context; @@ -143,7 +143,7 @@ package body RFLX.In_IPv4.Tests is Ethernet.Frame.Set_Source (Ethernet_Frame_Context, 16#000000000000#); Ethernet.Frame.Set_Type_Length_TPID (Ethernet_Frame_Context, 16#0800#); Ethernet.Frame.Set_Type_Length (Ethernet_Frame_Context, 16#0800#); - Ethernet.Frame.Initialize_Bounded_Payload (Ethernet_Frame_Context, 368); + Ethernet.Frame.Initialize_Payload (Ethernet_Frame_Context); Assert (Ethernet.Frame.Structural_Valid_Message (Ethernet_Frame_Context), "Structural invalid frame"); Assert (not Ethernet.Frame.Valid_Message (Ethernet_Frame_Context), "Valid frame"); @@ -184,8 +184,10 @@ package body RFLX.In_IPv4.Tests is UDP.Datagram.Take_Buffer (UDP_Datagram_Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (UDP_Datagram_Context.Last) - - RFLX_Types.Byte_Index (Ethernet_Frame_Context.First) + 1), Expected'Length'Img, + Assert (RFLX_Builtin_Types.Length'Image + (RFLX_Types.Byte_Index (UDP.Datagram.Message_Last (UDP_Datagram_Context)) + - RFLX_Types.Byte_Index (Ethernet_Frame_Context.First) + 1), + Expected'Length'Img, "Invalid buffer length"); Assert (Buffer.all (RFLX_Types.Byte_Index (Ethernet_Frame_Context.First) .. RFLX_Types.Byte_Index (Ethernet_Frame_Context.Last)), Expected.all, diff --git a/tests/spark/rflx-ipv4-tests.adb b/tests/spark/rflx-ipv4-tests.adb index 6741b1e211..65d0705b39 100644 --- a/tests/spark/rflx-ipv4-tests.adb +++ b/tests/spark/rflx-ipv4-tests.adb @@ -325,10 +325,14 @@ package body RFLX.IPv4.Tests is IPv4.Packet.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) - - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (IPv4.Packet.Message_Last (Context)) + - RFLX_Types.Byte_Index (Context.First) + 1), + Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), Expected.all, + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (IPv4.Packet.Message_Last (Context))), + Expected.all, "Invalid binary representation"); Free_Bytes_Ptr (Expected); @@ -357,10 +361,14 @@ package body RFLX.IPv4.Tests is IPv4.Option.Take_Buffer (Context, Buffer); - Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (Context.Last) - - RFLX_Types.Byte_Index (Context.First) + 1), Expected'Length'Img, + Assert (RFLX_Builtin_Types.Length'Image (RFLX_Types.Byte_Index (IPv4.Option.Message_Last (Context)) + - RFLX_Types.Byte_Index (Context.First) + 1), + Expected'Length'Img, "Invalid buffer length"); - Assert (Buffer.all (RFLX_Types.Byte_Index (Context.First) .. RFLX_Types.Byte_Index (Context.Last)), Expected.all, + Assert (Buffer.all + (RFLX_Types.Byte_Index (Context.First) + .. RFLX_Types.Byte_Index (IPv4.Option.Message_Last (Context))), + Expected.all, "Invalid binary representation"); Free_Bytes_Ptr (Expected);