[klee-dev] Strange value of uninitialized local variable

[xdb at seg.nju.edu.cn]

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?