Insufficient model verification regarding comparisons of opaque fields

[treiher]

It is possible to use comparisons of fields with opaque type which are not supported by the generated SPARK code. Here is an example:

package Test is

   type Message is
      message
         null
            then Foo
               with Length => 2;
         Foo : Opaque
            then null
               if Foo = 1;
      end message;

end Test;

Fields with opaque type should only be compared with aggregates, if their field size is a multiple of 8. A comparison with numeric literals shouldn't be possible at all.