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
<mailto: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