Allow adding a global invariant to a message

[jklmnn]

Some invariants are valid for a whole message including all its paths. Instead of adding these to all links to the final field separately a shortcut should be available.
Instead of:

package Test is

   type T is mod 2**8;

   type Test is
      message
         A : T
            then B
               with Size => A * 8
               if Size > 0;
            then null
               if Size = 0 and Message'Size mod 8 = 0;
         B : Opaque
            then null
               if Message'Size mod 8 = 0;
      end message;
end Test;

a predicate aspect can be used:

package Test is

   type T is mod 2**8;

   type Test is
      message
         A : T
            then B
               with Size => A * 8
               if Size > 0;
            then null
               if Size = 0;
         B : Opaque;
      end message with
         Predicate => Message'Size mod 8 = 0;

end Test;

[treiher]

         B : Opaque;
      end message;
end Test with
   Predicate => Message'Size mod 8 = 0;

The predicate should be at the message, not at the package.