Unsatisfiable precondition for setter of opaque field

[treiher]

The generated setters for opaque fields cannot be used correctly, if the value of the opaque field is compared to an aggregate in a condition. A field condition has to be fulfilled when setting a field. In case of opaque fields the to be set value is not provided to Field_Condition, so that the condition cannot be fulfilled.

package Test is

   type Message is
      message
         A : Opaque
            with Size => 16
            then null
               if A = [1, 2];
      end message;

end Test;

[treiher]

O1 Ignore comparisons of aggregates in field conditions

− The validity of the opaque fields of the serialized message cannot be ensured.

O2 Handle opaque fields with comparison to aggregate similar to scalar fields

To be able to check the field condition when setting A, a copy of the provided data for A needs to be stored in Field_Dependent_Value:

   type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is
      record
         case Fld is
            when F_Initial | F_Final =>
               null;
            when F_A =>
               A_Value : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 1);
         end case;
      end record;

And the value can then be checked in Field_Condition:

   function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean is
     ((case Val.Fld is
          when F_Initial =>
             True,
          when F_A =>
             Val.A_Value = (1, 2),
          when F_Final =>
             False));

− While this works fine for procedure Set_A (Ctx : in out Context; Data : RFLX_Types.Bytes), the field condition cannot be checked when using generic setter generic with procedure Process_A (A : out RFLX_Types.Bytes); with function Valid_Length (Length : RFLX_Types.Length) return Boolean; procedure Generic_Set_A (Ctx : in out Context). Thus, the validity of the serialized message cannot be ensured.
− Parts of the buffer are copied into Field_Dependend_Value and thus also in Context.
− The size of Context increases.

---

I have already implemented O2, but the resulting implementation does not compile with -gnata because of a GNAT bug (cf. U519-020). I'm also not very happy about detecting affected fields by looking for fields with a comparison to an aggregate in a condition, but handling all fixed-size opaque fields equally would increase the negative impact of the buffer copies. Keeping copies in Context may be preventable by not reusing Field_Dependent_Value and just storing the bounds of the field there, but this would require major changes.