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

Re: [csmith-dev] possible bug



I noticed l_966 is a struct and is properly initialized. Therefore it should be allowed to read. I don’t know why is KCC complaining.

 

-Xuejun

 

 

From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of Pascal Cuoq
Sent: Thursday, August 11, 2011 8:54 AM
To: John Regehr
Cc: csmith-dev@flux.utah.edu
Subject: Re: [csmith-dev] possible bug

 

On Thu, Aug 11, 2011 at 4:20 PM, John Regehr <regehr@cs.utah.edu> wrote:

On x86, using the latest version, I'm making a random program like this:

csmith -s 1243108467 --bitfields --no-volatiles --no-packed-struct --no-longlong  --output rand005561.c


Assuming I got it right:
$ md5sum rand005561.c
01a61c845db363b3916088e2a0c2c6f7  rand005561.c


And turning it into small.c like this:

current-gcc -m32 -O0 -DUSE_MATH_MACROS_NOTMP -D__COMPCERT__   -w -DINLINE= -DCSMITH_MINIMAL  -I/mnt/z/csmith/runtime rand005561.c -E | grep -v '^#' > small.c

And kcc is saying this:

=============================================================
ERROR! KCC encountered an error while executing this program.
=============================================================
Error: 00006
Description: Reading unspecified (possibly uninitialized) memory, or trying to read a pointer or float through an integer type.
=============================================================
File: /mnt/z/volatile/bugs/tmp045/small.c
Function: func_16
Line: 1131


Line 1131 is:
l_983 ^= (l_982 = (safe_div_func_uint16_t_u_u((l_966 , (((g_440[0][3].f3 = (((*l_967) = func_32((*g_228), p_18)) , p_17)) && (safe_rshift_func_int8_t_s_u((safe_rshift_func_uint8_t_u_s((safe_sub_func_uint8_t_u_u((l_974 == ((*l_979) = ((*p_18) , g_976[2][1]))), ((safe_lshift_func_int8_t_s_u(((-2L) ^ p_17), p_17)) || (*g_182)))), 2)), g_74.f7))) >= 0xD18114D4L)), g_150.f2)));

l_966, on the left-hand side of a comma, contains some uninitialized bits.

        l_966.f0 ∈ {255}
             .[bits 18 to 23] ∈ UNINITIALIZED
             .f1 ∈ {-5}
             .f2 ∈ {10914}
             .f3 ∈ {1}
             .f4.f0 ∈ {-32387}
             .f4.[bits 16 to 31] ∈ UNINITIALIZED
             .f4.f1 ∈ {1558229903}
             .f4.f2 ∈ {539530558}
             .f4.f3 ∈ {5}
             .f4.f4 ∈ {-8}
             .f4.f5 ∈ {1}
             .f4.[bits 176 to 191] ∈ UNINITIALIZED
             .f4.f6 ∈ {4294967287}
             .f4.f7 ∈ {88}
             .f4.f8 ∈ {246}
             .f4.[bits 240 to 255] ∈ UNINITIALIZED
             .f5 ∈ {0}
             .f6 ∈ {33957}
             .[bits 368 to 383] ∈ UNINITIALIZED
             .f7 ∈ {2882519580}

Does KCC accept the programs below?

union U { char c ; int i; };

main(){
  union U l;
  return (l, 12);
}
_______________________

union U { char c ; int i; };

main(){
  union U l;
  l.c = 1;
  return (l, 12);
}

The value analysis accepts both. The second one is more like small.c and I would say it's defined without doubt. The first one, I do not know.

Pascal