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

>   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.


Yes, CHAR_BIT can be 8 or greater
... but I use uint8_t cast in my code. Look at "7.20.1.1 Exact-width integer types" 
>   The typedef name uintN_t designates an unsigned integer type with width N and no padding bits. Thus, uint24_t denotes such an unsigned integer type with a width of exactly 24 bits. Macro CHAR_BIT from limits.h defines the number of bits in a char.

Frama-C in it's internal "stdint.h" :

typedef unsigned char uint8_t;
typedef unsigned long long uint64_t;
typedef long long intmax_t;

 assumes that "unsigned char" and "uint8_t" is the same thing, but this wrong for some platform/compilers.

On come platform, "char" type can be "unsigned char" ->
"5.2.4.2.1  Sizes of integer types <limits.h>"

https://www.lysator.liu.se/c/rat/c1.html#3-1-2-5 :
>   Three types of char are specified: signed, plain, and unsigned. A plain char may be represented as either signed or unsigned, depending upon the implementation, as in prior practice. The type signed char was introduced to make available a one-byte signed integer type on those systems which implement plain char as unsigned. For reasons of symmetry, the keyword signed is allowed as part of the type name of other integral types.

Signed integers can be one's complement or two’s complement "6.2.6.2  Integer types" -> https://en.wikipedia.org/wiki/Signed_number_representations