[klee-dev] Strange value of uninitialized local variable

[Oscar Soria Dustmann]

Hi,

well, the value 12370169555311111083 needs 64 bits to be represented and
therefore just manages to fit in an 8-byte variable of type `long`.

As for where the value comes from, lib/Core/Memory.cpp defines
uninitialised memory to the "randomly chosen value" 0xAB:

265 void ObjectState::initializeToRandom() {
266   makeConcrete();
267   for (unsigned i=0; i<size; i++) {
268     // randomly selected by 256 sided die
269     concreteStore[i] = 0xAB;
270   }
271 }

Note: http://xkcd.com/221/

Best, Oscar

On 10/12/14 18:47, Jonathan Neuschäfer wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>