--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2016 ---
[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.