[klee-dev] how klee_set_forking works exactly?

[Sunha Ahn]

Hi, all.

I would like to know how exactly klee_set_forking works.

It seems like that, after klee_set_forking(0);, a branch controlled by a
symbolic variable is not forked with both true/false sides any more.
However, it still picks either one of the branch. I do not understand how
they pick when the symbolic variable is still symbolic.

For example,

1:  int x;
2:  klee_make_symbolic(&x, sizeof(x), "x");
3:  klee_assume(x>0);
4:  klee_assume(x<10);
5:  klee_set_forking(0);
6:
7:  if(x>5){
8:        printf("1\n");
9:  }else{
10:       printf("2\n");
11: }


Here, it prints "2".
At line 6, x is still symbolic, i.e. the value x can be either less than 5
or greater than 5. I do not understand how they choose the false branch.


Besides this example, I would appreciate any explanation on how
klee_set_forking works.


I always appreciate that you answer my questions!

Many many thanks,
Sunha.
-------------- next part --------------
HTML attachment scrubbed and removed