[RFA] Setting long long bitfields

[Paul N. Hilfinger]

> How can bitsize ever become zero?  Note that the original code contains a
> shift by bitsize - 1, which is undefined as well in this case.

Actually, Ada programs, unlike C, can generate fields of width 0.  I see,
however, that (somewhat accidentally) that case is handled as a 0-byte
ordinary byte-aligned field (where the alignment doesn't matter, of course,
since 0 bytes of data are modified).  Very well, I will adopt Andreas'
suggestion, and also document the precondition in the comment.  

Thanks.

Paul