data structure size chosen by klee?

[Mark R. Tuttle]

Is there a "right" way to ask klee to choose the size of a data structure?

I'm used to a different symbolic tool, and I'm used to writing a test bench
that might be equivalent to

int main() {
int size = klee_int("size");
int array[size];
for (int i=0;i<size;i++) {array[i] = klee_int("array");}

sort(array,size);
return 1;
}

but klee points to the array declaration and complains with

WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: NOTE: found huge malloc, returning 0
KLEE: ERROR: /nfs/site/home/mrtuttle/shr/uefi/ddt/question1.c:5:
concretized symbolic size
KLEE: NOTE: now ignoring this error at this location

Related questions:

Q1: I understand that klee does not currently support symbolic arguments to
malloc, and klee concretizes the symbolic value. How is this concrete
value chosen? Is it fixed for all successor states? Where can I read more
about this process of concretizing values and how klee does it?

Q2: I was surprised to see the "does not support the llvm.stacksave
intrinsic" warning message. I'm using LLVM 2.9 and the llvm-gcc for LLVM
2.9, I'm using the latest versions of stp and klee from their
repositories. Does this error message suggest that I built something
incorrectly? I'm using version 2.9 and not 3.3 because I understand that
is the most used (stress-tested) configuration for klee.

Q3: A naive application of klee to quicksort (similar to the test bench
above) runs longer than my patience, generating thousands of tests for a
short array. Is klee trying to do full path coverage? Is klee going to
try to generate every input permutation needed to exercise every path
through the sort algorithm? I'm used to a different symbolic tool that
does branch coverage (exercise every branch in both directions) and not
path coverage, and there are heuristics to get that tool to terminate
quickly. Are there heuristics for klee documented somewhere that I should
study to help bound the execution of klee?

Thanks,
Mark