Condition from Initial to first field

[senier]

The following message is currently considered valid:

   type M is
      message
         null
            then F
               if Message'Length < 20;
            F : Boolean;
      end message;

I don't see any useful applications for the first condition as only static expressions or message attributes may be referenced (and I'm not even sure whether the above example would produce any sensible SPARK code).

@treiher Maybe we want to reject conditions for the edge starting at Initial? I'm thinking about this in the context of merging messages and allowing those condition would complicated things further.

[treiher]

I cannot think of a valid use case either. We should reject such conditions.

[senier]

This has become obsolete by the introduction of parameterize message. @treiher Should be close this ticket?

[treiher]

As the message shown above is still accepted as valid, we still have to add a check which rejects such specifications.

[senier]

Ref. #764

[treiher]

We decided in #764 to allow conditions on initial links.