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

Re: [csmith-dev] subtle signed overflow issue

Nice catch, guys!

Although this case is undefined, I feel like there are probably some well-defined cases "near" this one that a lot of compilers are going to get wrong...

Xuejun, what are your current rules for saying ++x is OK? How do you think they should be changed in order to disallow this case, while allowing similar (but well-defined) constructs?


On 10/12/11 9:35 AM, Chucky Ellison wrote:
 >From n1570 ( <>): "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.


2011/10/12 Pascal Cuoq <pascal.cuoq@gmail.com


    Here is a new, extremely interesting program generated by Csmith:

      * 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 };

       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?