Ada/SPARK: Uninitialized out parameters cause gnatprove warnings

[sbenitezb]

Generated code like the following, which includes SPARK annotations, when ran against gnatprove (default settings), causes tons of medium warnings due to uninitialized out parameters:

ipc_base.ads:329:36: medium: "val.sequenceNumber" might not be initialized in "MessageHeader_Decode_aux"
  329 |procedure MessageHeader_Decode_aux(val: out MessageHeader; bs : in out adaasn1rtl.encoding.Bitstream; result : OUT adaasn1rtl.ASN1_RESULT)
      |                                   ^~~
  reason for check: OUT parameter should be fully initialized on return
  possible fix: initialize "val.sequenceNumber" on all paths, make "val" an IN OUT parameter or annotate it with aspect Relaxed_Initialization

ipc_base.ads:329:36: medium: "val.timestamp.seconds" might not be initialized in "MessageHeader_Decode_aux"
  329 |procedure MessageHeader_Decode_aux(val: out MessageHeader; bs : in out adaasn1rtl.encoding.Bitstream; result : OUT adaasn1rtl.ASN1_RESULT)
      |                                   ^~~
  reason for check: OUT parameter should be fully initialized on return
  possible fix: initialize "val.timestamp.seconds" on all paths, make "val" an IN OUT parameter or annotate it with aspect Relaxed_Initialization

ipc_base.ads:329:36: medium: "val.timestamp.nanoseconds" might not be initialized in "MessageHeader_Decode_aux"
  329 |procedure MessageHeader_Decode_aux(val: out MessageHeader; bs : in out adaasn1rtl.encoding.Bitstream; result : OUT adaasn1rtl.ASN1_RESULT)
      |                                   ^~~
  reason for check: OUT parameter should be fully initialized on return
  possible fix: initialize "val.timestamp.nanoseconds" on all paths, make "val" an IN OUT parameter or annotate it with aspect Relaxed_Initialization

procedure MessageHeader_Decode(val: out MessageHeader; Stream : in out MessageHeader_uPER_Stream; result : OUT adaasn1rtl.ASN1_RESULT);
procedure MessageHeader_Decode_aux(val: out MessageHeader; bs : in out adaasn1rtl.encoding.Bitstream; result : OUT adaasn1rtl.ASN1_RESULT)
with
    Pre => bs.Current_Bit_Pos < Natural'Last - MessageHeader_REQUIRED_BITS_FOR_ENCODING
      and then bs.Size_In_Bytes < Positive'Last / 8
      and then bs.Current_Bit_Pos + MessageHeader_REQUIRED_BITS_FOR_ENCODING <= bs.Size_In_Bytes * 8,
       Post =>
         bs.Current_Bit_Pos >= bs'Old.Current_Bit_Pos and bs.Current_Bit_Pos <= bs'Old.Current_Bit_Pos + MessageHeader_REQUIRED_BITS_FOR_ENCODING
;

procedure MessageHeader_Decode_aux(val: out MessageHeader; bs : in out adaasn1rtl.encoding.Bitstream; result : OUT adaasn1rtl.ASN1_RESULT)
is

begin
    -- val := MessageHeader_Init;

    --Decode version
    result.ErrorCode := ERR_UPER_DECODE_MESSAGEHEADER_VERSION;
    adaasn1rtl.encoding.uper.UPER_Dec_UnConstraintWholeNumber(bs, val.version, result.Success);
    if result.Success then
        --Decode timestamp
        TTIMESTAMP_Decode_aux(val.timestamp, bs, result);
        if result.Success then
            --Decode sequenceNumber
            MessageId_Decode_aux(val.sequenceNumber, bs, result);
        end if;
    end if;
end MessageHeader_Decode_aux;

procedure MessageHeader_Decode(val:out MessageHeader; Stream : IN OUT MessageHeader_uPER_Stream; result : OUT adaasn1rtl.ASN1_RESULT)
is
begin
    Stream.Current_Bit_Pos :=0;
    MessageHeader_Decode_aux(val, Stream, result);
    if result.success then
        result := MessageHeader_IsConstraintValid(val);
    end if;

end MessageHeader_Decode;

For some reason, the initialization of val is commented out:

asn1scc/StgAda/uper_a.stg

Line 126 in d4e928e

-- <sVarName> := <soInitFuncName>;

).

Shouldn't these be in out if initialized elsewhere, or initialized inside the procedure, if kept out only?