Verification of size compatibility for refinements

[treiher]

It should be verified if an inner message fits into the refined opaque field of the outer message. A refinement should be rejected, if the inner message is too small or too big. Inner messages and refined opaque fields with variable sizes as well as size constraints in the refinement condition must be considered.

Here is a simple example where the inner message is too big for the refined field:

package Test is

   type U16 is mod 2 ** 16;

   type M1 is
      message
         A : U16;
      end message;

   type M2 is
      message
         A : Opaque
            with Size => 8;
      end message;

   for M2 use (A => M1);

end Test;

[jklmnn]

The same problem exists with message types:

package Test is

   type U16 is mod 2**16;

   type M1 is
      message
         A : U16;
      end message;

   type M2 is
      message
         A : M1
            with Size => 8;
      end message;

end Test;

This is also checked as valid although there is no valid path to FINAL.

EDIT: This is a separate problem and is handled in #546.