[klee-dev] Making memory space partially symbolic

[sudiptac]

Dear All,
     Let us assume that we have a large piece of memory, say 128 bytes 
of an array.
What is the right way to make some (but not all) part of this array to 
be symbolic?

     More precisely, I can identify the memory object created for an 
array in KLEE
code. I wish to make a fraction of the memory space occupied by this 
array to be
symbolic.

     In general, SpecialFunctionaHandler.cpp check for the size in 
klee_make_symbolic
calls. Therefore, it seems changing the size parameter in 
klee_make_symbolic call
is not a good option.

     Any help or pointer is greatly appreciated.

Regards,
Sudipta