Hi Pascal, this is fixed in commit a39f3c. Thanks for catching my wrong assumption. -Xuejun From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of Xuejun Yang Sent: Friday, August 05, 2011 11:26 AM To: 'Pascal Cuoq'; csmith-dev@flux.utah.edu Subject: Re: [csmith-dev] Unions in C program: referee needed Thanks Pascal for a tricky Csmith bug. I am working on it. -Xuejun From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of Pascal Cuoq Sent: Friday, August 05, 2011 8:18 AM To: csmith-dev@flux.utah.edu Subject: [csmith-dev] Unions in C program: referee needed Hello,
something funny is happening with a Csmith-generated program. Csmith claims it is defined (I think. I didn't use dangerous options), Frama-C's value analysis thinks it's not, and I am not quite sure how to arbitrate between them.
This is with version, options and seed:
* Git version: 01a9384 * Options: --max-pointer-depth 3 --max-funcs 2 --max-array-dim 2 --max-array-len-per-dim 3 --max-struct-fields 5 --no-volatiles --no-argc --unions * Seed: 1647756027
Executing the program works fine (with 64-bit, little-endian GCC): checksum = 682193FB
On the other hand, the value analysis chokes shortly after line 628: transparent_crc(g_118.f0, "g_118.f0", print_hash_value);
Instrumenting the program to get details, it says it thinks that at that point:
g_118{.f0[bits 0 to 7]; .f1.f0; .f2.f0.f0.f0; .f3.f0.f0.f0[bits 0 to 7]; } ∈ {77} {.f0[bits 8 to 31]; .f1.[bits 8 to 31]; .f2.f0.f0.[bits 8 to 31]; .f3.f0.f0{.f0[bits 8 to 15]; .f1; }; } ∈ UNINITIALIZED {.f0[bits 32 to 63]; .f1.[bits 32 to 63]; .f2.f0.f0.f1; .f3.f0.f0.f2; } ∈ {2683586253} {.f0[bits 64 to 71]; .f1; .f2.f0.f0.f2; .f3.f0.f1[bits 0 to 7]; } ∈ {0} {.f0[bits 72 to 95]; .f1.[bits 72 to 95]; .f2.f0.f0.[bits 72 to 95]; .f3.f0.f1[bits 8 to 31]; } ∈ UNINITIALIZED {.f0[bits 96 to 447]; .f1.[bits 96 to 447]; .f2.[bits 96 to 447]; .f3{.f0{.f1[bits 32 to 63]; .f2; .[bits 224 to 255]; }; .f1; .f2; .f3; .[bits 288 to 319]; }; } ∈ {0}
There are quite a few uninitialized bits in member g_118.f0, so it is right to complain, but the question is whether the values it has computed can be trusted.
My computer does not support the awatch command in GDB for some reason, so I am a little naked here. The best continuation I know is:
$ gdb a.out ... (gdb) break transparent_crc Breakpoint 1 at 0x4016f3: file runtime/csmith.h, line 113. (gdb) run Starting program: /home/cuoq/csmith_new/a.out
Breakpoint 1, transparent_crc (val=123, vname=0x403688 "g_4.f0.f0.f0", flag=0) at runtime/csmith.h:113 113 crc32_8bytes(val); (gdb) print g_118 $1 = {f0 = 11525915192630181965, f1 = {f0 = 77 'M'}, f2 = {f0 = {f0 = {f0 = 77 'M', f1 = 2683586253, f2 = 0 '\000'}}}, f3 = {f0 = {f0 = {f0 = 77, f1 = 0, f2 = 2683586253}, f1 = 0, f2 = {f0 = 0 '\000', f1 = 0, f2 = 0 '\000'}}, f1 = 0, f2 = 0, f3 = 0}}
So execution and analysis seem to agree for the members that are initialized. Does anyone know how to determine for sure whether the second byte (for instance) is initialized or not? I tried executing twice, but the same result comes out (which does not prove anything. The program is deterministic and the stack may naturally always hold the same values part of it is used without initialization).
Pascal
|