Question about KLEE

[Mingyue Jiang]

Hi All,

I'm new to KLEE.
I have three questions about KLEE.


(1) How to get the symbolic output related to each path.

For example, consider following program.

Int large(int a, int b)

{

Int x;

If(a>b)

X=a;

Else

X=b;

Return x;

}
Main()
{
Int a,b;
Klee_make_symbolic(&a,sizeof(a),"a");
Klee_make_symbolic(&b,sizeof(b),"b");
Return large(a,b);
}
With KLEE, I can get 2 test cases and their corresponding path conditions: a>b and a<=b.
But, I want to see its symbolic output of each path, i.e,, the output is "a" with path condition "a>b".
How can KLEE produce this kind of information? Any options should be used?


(2) I'm quite confused about options related to -posix-runtime.

For example, --sym-args 0 2 10, this argument maximumly generate 2 symbolic arguments whose length is 10.

The first(second) generated symbolic arguments represents the first(second) argument in main(), is that right?



When -posix-runtime is used, I always get unexpected results. I wonder under which situation this option is recommended to be used.



(3) How to execute programs contains file operation (i.e., open file, read file, etc.) with KLEE.



Can this kinds of programs can be processed without -posix-runtime options, if yes, which options can be used to process it.


Any help is truly appreciated. Thanks.

Best regards,

Mingyue Jiang