Allow setting empty sequence field

Ref. #353
AdaCore · Jul 23, 2020 · e6d5b28 · e6d5b28
1 parent bb71f70
commit e6d5b28
Show file tree

Hide file tree

Showing 24 changed files with 467 additions and 131 deletions.
diff --git a/generated/rflx-arrays-generic_inner_message.adb b/generated/rflx-arrays-generic_inner_message.adb
@@ -394,6 +394,16 @@ is
       Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length);
    end Set_Length;
 
+   procedure Set_Payload_Empty (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.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;
+
    procedure Set_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);

diff --git a/generated/rflx-arrays-generic_inner_message.ads b/generated/rflx-arrays-generic_inner_message.ads
@@ -218,6 +218,27 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   procedure Set_Payload_Empty (Ctx : in out Context) 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))
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Payload) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Payload) = 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 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
+       and Structural_Valid (Ctx, F_Payload);
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;

diff --git a/generated/rflx-arrays-generic_message.adb b/generated/rflx-arrays-generic_message.adb
@@ -583,6 +583,16 @@ is
       Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length);
    end Set_Length;
 
+   procedure Set_Modular_Vector_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Modular_Vector);
+      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.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;
+
    procedure Switch_To_Modular_Vector (Ctx : in out Context; Seq_Ctx : out Modular_Vector_Sequence.Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Modular_Vector);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Modular_Vector);

diff --git a/generated/rflx-arrays-generic_message.ads b/generated/rflx-arrays-generic_message.ads
@@ -247,6 +247,32 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   procedure Set_Modular_Vector_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Modular_Vector)
+       and then Field_Last (Ctx, F_Modular_Vector) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_Modular_Vector))
+       and then Available_Space (Ctx, F_Modular_Vector) >= Field_Length (Ctx, F_Modular_Vector)
+       and then Field_First (Ctx, F_Modular_Vector) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Modular_Vector) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Modular_Vector) = 0,
+     Post =>
+       Has_Buffer (Ctx)
+       and Invalid (Ctx, F_Range_Vector)
+       and Invalid (Ctx, F_Enumeration_Vector)
+       and Invalid (Ctx, F_AV_Enumeration_Vector)
+       and (Predecessor (Ctx, F_Range_Vector) = F_Modular_Vector
+            and Valid_Next (Ctx, F_Range_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_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
+       and Structural_Valid (Ctx, F_Modular_Vector);
+
    procedure Switch_To_Modular_Vector (Ctx : in out Context; Seq_Ctx : out Modular_Vector_Sequence.Context) with
      Pre =>
        not Ctx'Constrained

diff --git a/generated/rflx-arrays-generic_messages_message.adb b/generated/rflx-arrays-generic_messages_message.adb
@@ -394,6 +394,16 @@ is
       Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length);
    end Set_Length;
 
+   procedure Set_Messages_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Messages);
+      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.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;
+
    procedure Switch_To_Messages (Ctx : in out Context; Seq_Ctx : out Inner_Messages_Sequence.Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Messages);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Messages);

diff --git a/generated/rflx-arrays-generic_messages_message.ads b/generated/rflx-arrays-generic_messages_message.ads
@@ -220,6 +220,27 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   procedure Set_Messages_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Messages)
+       and then Field_Last (Ctx, F_Messages) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_Messages))
+       and then Available_Space (Ctx, F_Messages) >= Field_Length (Ctx, F_Messages)
+       and then Field_First (Ctx, F_Messages) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Messages) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Messages) = 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 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
+       and Structural_Valid (Ctx, F_Messages);
+
    procedure Switch_To_Messages (Ctx : in out Context; Seq_Ctx : out Inner_Messages_Sequence.Context) with
      Pre =>
        not Ctx'Constrained

diff --git a/generated/rflx-ipv4-generic_option.adb b/generated/rflx-ipv4-generic_option.adb
@@ -736,6 +736,16 @@ is
       Ctx.Cursors (Successor (Ctx, F_Option_Length)) := (State => S_Invalid, Predecessor => F_Option_Length);
    end Set_Option_Length;
 
+   procedure Set_Option_Data_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Option_Data);
+      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.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;
+
    procedure Set_Option_Data (Ctx : in out Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Option_Data);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Option_Data);

diff --git a/generated/rflx-ipv4-generic_option.ads b/generated/rflx-ipv4-generic_option.ads
@@ -340,6 +340,30 @@ is
        and Context_Cursor (Ctx, F_Option_Class) = Context_Cursor (Ctx, F_Option_Class)'Old
        and Context_Cursor (Ctx, F_Option_Number) = Context_Cursor (Ctx, F_Option_Number)'Old;
 
+   procedure Set_Option_Data_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Option_Data)
+       and then Field_Last (Ctx, F_Option_Data) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_Option_Data))
+       and then Available_Space (Ctx, F_Option_Data) >= Field_Length (Ctx, F_Option_Data)
+       and then Field_First (Ctx, F_Option_Data) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Option_Data) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Option_Data) = 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 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
+       and Get_Option_Class (Ctx) = Get_Option_Class (Ctx)'Old
+       and Get_Option_Number (Ctx) = Get_Option_Number (Ctx)'Old
+       and Get_Option_Length (Ctx) = Get_Option_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_Option_Data);
+
    generic
       with procedure Process_Option_Data (Option_Data : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;