Scalars with size greater than 57 bit

[treiher]

package Test is

   type U58 is mod 2**58;

   type Message is
      message
         F1 : U58;
      end message;

end Test;

rflx-test-generic_message.adb:184:48: medium: precondition might fail, cannot prove Natural (((Offset'Pos (Ofst) + Value'Size - 1) / Byte'Size) * Byte'Size) < Long_Integer'Size - 1, in instantiation at rflx-test-message.ads:6

While the generated code for the simple example shown above can be successfully verified for integers up to a size of 57 bit, it fails with bigger ones. Increasing the proof steps and the timeout to --steps=100000 --timeout=120 did not help.

[treiher]

The failing precondition is needed to prevent some overflows in the implementation of Extract. I see no simple solution for this problem at the moment. This issue should be address in the context of #182.