Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t

Mohamed Iguernlala wrote:
> return ((a)%256 == (unsigned char)(a));

I was going to go into language lawyer mode and point out that a char is
specified to be one byte, but a byte isn't specified to 8 bits. However,
since at least 2003 POSIX states:

> The values for the limits {CHAR_BIT}, {SCHAR_MAX}, and {UCHAR_MAX} are
> now required to be 8, +127, and 255, respectively.
> 
> The value for the limit {CHAR_MAX} is now {UCHAR_MAX} or {SCHAR_MAX}.

http://pubs.opengroup.org/onlinepubs/9699919799/basedefs/limits.h.html

So does C11:

http://www.open-std.org/jtc1/sc22/WG14/www/docs/n1570.pdf

And casting trunction is defined in terms of *_MAX. So that expression
seems to be reliably defined as long as a >= 0.