Allow setting empty sequence field

Ref. #353
AdaCore · Jul 27, 2020 · ad632a6 · ad632a6
1 parent 591298b
commit ad632a6
Show file tree

Hide file tree

Showing 28 changed files with 669 additions and 132 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,31 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   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);
+
+   pragma Warnings (On, "precondition is always False");
+
    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,46 @@ 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 Set_Range_Vector_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Range_Vector);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_Range_Vector);
+   begin
+      Reset_Dependent_Fields (Ctx, F_Range_Vector);
+      Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors);
+      Ctx.Cursors (F_Range_Vector) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Range_Vector), Predecessor => Ctx.Cursors (F_Range_Vector).Predecessor);
+      Ctx.Cursors (Successor (Ctx, F_Range_Vector)) := (State => S_Invalid, Predecessor => F_Range_Vector);
+   end Set_Range_Vector_Empty;
+
+   procedure Set_Enumeration_Vector_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Enumeration_Vector);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_Enumeration_Vector);
+   begin
+      Reset_Dependent_Fields (Ctx, F_Enumeration_Vector);
+      Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors);
+      Ctx.Cursors (F_Enumeration_Vector) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Enumeration_Vector), Predecessor => Ctx.Cursors (F_Enumeration_Vector).Predecessor);
+      Ctx.Cursors (Successor (Ctx, F_Enumeration_Vector)) := (State => S_Invalid, Predecessor => F_Enumeration_Vector);
+   end Set_Enumeration_Vector_Empty;
+
+   procedure Set_AV_Enumeration_Vector_Empty (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_AV_Enumeration_Vector);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_AV_Enumeration_Vector);
+   begin
+      Reset_Dependent_Fields (Ctx, F_AV_Enumeration_Vector);
+      Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, Ctx.First, Last, Ctx.Buffer, Ctx.Cursors);
+      Ctx.Cursors (F_AV_Enumeration_Vector) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_AV_Enumeration_Vector), Predecessor => Ctx.Cursors (F_AV_Enumeration_Vector).Predecessor);
+      Ctx.Cursors (Successor (Ctx, F_AV_Enumeration_Vector)) := (State => S_Invalid, Predecessor => F_AV_Enumeration_Vector);
+   end Set_AV_Enumeration_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,106 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   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 Set_Range_Vector_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Range_Vector)
+       and then Field_Last (Ctx, F_Range_Vector) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_Range_Vector))
+       and then Available_Space (Ctx, F_Range_Vector) >= Field_Length (Ctx, F_Range_Vector)
+       and then Field_First (Ctx, F_Range_Vector) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Range_Vector) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Range_Vector) = 0,
+     Post =>
+       Has_Buffer (Ctx)
+       and Invalid (Ctx, F_Enumeration_Vector)
+       and Invalid (Ctx, F_AV_Enumeration_Vector)
+       and (Predecessor (Ctx, F_Enumeration_Vector) = F_Range_Vector
+            and Valid_Next (Ctx, F_Enumeration_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_Range_Vector) = Predecessor (Ctx, F_Range_Vector)'Old
+       and Valid_Next (Ctx, F_Range_Vector) = Valid_Next (Ctx, F_Range_Vector)'Old
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_Range_Vector);
+
+   procedure Set_Enumeration_Vector_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Enumeration_Vector)
+       and then Field_Last (Ctx, F_Enumeration_Vector) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_Enumeration_Vector))
+       and then Available_Space (Ctx, F_Enumeration_Vector) >= Field_Length (Ctx, F_Enumeration_Vector)
+       and then Field_First (Ctx, F_Enumeration_Vector) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_Enumeration_Vector) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_Enumeration_Vector) = 0,
+     Post =>
+       Has_Buffer (Ctx)
+       and Invalid (Ctx, F_AV_Enumeration_Vector)
+       and (Predecessor (Ctx, F_AV_Enumeration_Vector) = F_Enumeration_Vector
+            and Valid_Next (Ctx, F_AV_Enumeration_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_Enumeration_Vector) = Predecessor (Ctx, F_Enumeration_Vector)'Old
+       and Valid_Next (Ctx, F_Enumeration_Vector) = Valid_Next (Ctx, F_Enumeration_Vector)'Old
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_Enumeration_Vector);
+
+   procedure Set_AV_Enumeration_Vector_Empty (Ctx : in out Context) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_AV_Enumeration_Vector)
+       and then Field_Last (Ctx, F_AV_Enumeration_Vector) <= Types.Bit_Index'Last / 2
+       and then Field_Condition (Ctx, (Fld => F_AV_Enumeration_Vector))
+       and then Available_Space (Ctx, F_AV_Enumeration_Vector) >= Field_Length (Ctx, F_AV_Enumeration_Vector)
+       and then Field_First (Ctx, F_AV_Enumeration_Vector) mod Types.Byte'Size = 1
+       and then Field_Length (Ctx, F_AV_Enumeration_Vector) mod Types.Byte'Size = 0
+       and then Field_Length (Ctx, F_AV_Enumeration_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 Predecessor (Ctx, F_AV_Enumeration_Vector) = Predecessor (Ctx, F_AV_Enumeration_Vector)'Old
+       and Valid_Next (Ctx, F_AV_Enumeration_Vector) = Valid_Next (Ctx, F_AV_Enumeration_Vector)'Old
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_AV_Enumeration_Vector);
+
+   pragma Warnings (On, "precondition is always False");
+
    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,31 @@ is
        and Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
        and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   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);
+
+   pragma Warnings (On, "precondition is always False");
+
    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-enumeration-generic_message.ads b/generated/rflx-enumeration-generic_message.ads
@@ -203,6 +203,10 @@ is
        and Predecessor (Ctx, F_Priority) = Predecessor (Ctx, F_Priority)'Old
        and Valid_Next (Ctx, F_Priority) = Valid_Next (Ctx, F_Priority)'Old;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   pragma Warnings (On, "precondition is always False");
+
    function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor with
      Annotate =>
        (GNATprove, Inline_For_Proof),

diff --git a/generated/rflx-ethernet-generic_frame.adb b/generated/rflx-ethernet-generic_frame.adb
@@ -907,6 +907,16 @@ is
       Ctx.Cursors (Successor (Ctx, F_Type_Length)) := (State => S_Invalid, Predecessor => F_Type_Length);
    end Set_Type_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-ethernet-generic_frame.ads b/generated/rflx-ethernet-generic_frame.ads
@@ -417,6 +417,34 @@ is
        and Context_Cursor (Ctx, F_TPID) = Context_Cursor (Ctx, F_TPID)'Old
        and Context_Cursor (Ctx, F_TCI) = Context_Cursor (Ctx, F_TCI)'Old;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   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), Field_Length (Ctx, 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_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);
+
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;

diff --git a/generated/rflx-expression-generic_message.adb b/generated/rflx-expression-generic_message.adb
@@ -266,6 +266,16 @@ is
       Process_Payload (Ctx.Buffer.all (First .. Last));
    end Get_Payload;
 
+   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-expression-generic_message.ads b/generated/rflx-expression-generic_message.ads
@@ -190,6 +190,30 @@ is
        Has_Buffer (Ctx)
        and Present (Ctx, F_Payload);
 
+   pragma Warnings (Off, "precondition is always False");
+
+   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 Structural_Valid (Ctx, F_Payload);
+
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;