Appending independently created messages to array

[treiher]

The generated SPARK code does not allow appending independently created messages to an array. This is heavily used in our current TLS session specification:

         Post_Handshake_Auth_Extension : TLS_Handshake::CH_Extension;
      begin
         Post_Handshake_Auth_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_POST_HANDSHAKE_AUTH, Data_Length => 0, Data => []);
         Extensions_List'Append (Post_Handshake_Auth_Extension);

But I couldn't find any instance where it is strictly necessary and could not be replaced by:

      begin
         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_POST_HANDSHAKE_AUTH, Data_Length => 0, Data => []));

Either we have to prohibit appending independently created messages to an array in the session model or extend the code generator. The former solution is easy to implement and sufficient for now, while the latter provides more flexibility in the long-term.

[treiher]

In a separate discussion we decided to prohibit appending independently created messages to an array for now.