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
|