[klee-dev] Strange value of uninitialized local variable

[Jonathan Neuschäfer]

On Sat, Nov 22, 2014 at 12:56:27PM +0800, xdb at seg.nju.edu.cn wrote:
> Hi all,
> just use the following tiny program to illustrate my question
> 
>   int main(int argc, char **argv){
>        long a;
>        printf("value of a is %ld\n", a);
>       return 0;
>    }
> 
> When running the program with KLEE, I got the following output:
> klee --libc=uclibc --posix-runtime test.bc
> KLEE: NOTE: Using klee-uclibc : /usr/local/lib/klee-uclibc.bca
> KLEE: NOTE: Using model: /usr/local/lib/libkleeRuntimePOSIX.bca
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 26542160)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: calling external: printf(18269440, 12370169555311111083)
> value of a is -6076574518398440533
> 
> My question is that 12370169555311111083 cannot be represented by a long
> variable.
> Why KLEE assigns such value to an uninitialized local variable?
> Can anyone tell me how KLEE handles uninitialized local variables?


This number is 0xabababababababab when written in hexadecimal. I think a
part of KLEE (or LLVM) assigns an 0xab pattern to uninitialized memory
to make it easy to spot, but I have not read the relevant parts of the
code.

Jonathan