>From n1570 (6.3.1.1:2 <http://6.3.1.1:2>): "If an int can represent
all values of the original type (as restricted by the width, for a
bit-field), the value is converted to an int". It seems this is the
case with a 31 bit unsigned bitfield.
KCC also flags this as signed overflow.
-Chucky
2011/10/12 Pascal Cuoq <pascal.cuoq@gmail.com
<mailto:pascal.cuoq@gmail.com>>
Hello.
Here is a new, extremely interesting program generated by Csmith:
/*
* This is a RANDOMLY GENERATED PROGRAM.
*
* Generator: csmith 2.1.0
* Git version: a5e5fd1
* Options: --max-expr-complexity 15 --max-pointer-depth 3
--max-funcs 4 --max-array-dim 2 --max-array-len-per-dim 3
--max-struct-fields 12 --max-union-fields 12 --no-volatiles
--bitfields --no-argc --unions
* Seed: 1904236191
*/
A reduced version is like this:
union U4 { unsigned f0 : 31; } u = { -1 };
main(){
++u.f0;
return 0;
}
Frama-C's value analysis with option -val-signed-overflow-alarms says:
/home/cuoq/r.c:5:[kernel] warning: Signed overflow. assert
(int)u.f0+1 ≤ 2147483647LL;
Its reasoning is that ++u.f0 can be expanded into u.f0 = ((int)u.f0)
+ 1; and that the
addition takes places between signed ints, and is therefore subject
to undefined
overflows, one of which just happens to take place in this program.
What do you think?
Pascal