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