Re: [csmith-dev] subtle signed overflow issue

[Chucky Ellison <celliso2@illinois.edu>]

>From n1570 (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>

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