[klee-dev] how klee_set_forking works exactly?

[Sunha Ahn]

Hi, Daniel.
Thanks for the reply!

However, I feel like it might not be totally random.

For example,

----
  int x;
  klee_make_symbolic(&x, sizeof(x), "x");
  klee_assume(x>0);
  klee_set_forking(0);

  if(x<=0){
        printf("1\n");
  }else{
        printf("2\n");
  }
-----

In this case, KLEE chooses the false path and prints "2".

----
  int x;
  klee_make_symbolic(&x, sizeof(x), "x");
  klee_assume(x>0);
  klee_set_forking(0);

  if(x>0){
        printf("1\n");
  }else{
        printf("2\n");
  }
-----

In this case, KLEE chooses the true path and prints "1".

Does it chooses totally randomly? Seems like it knows some information.

Thanks a lot!

Best regards,
Sunha.



2013/6/21 Daniel Dunbar <daniel at zuster.org>

> If I recall correctly, KLEE will just randomly (based on a fixed seed,
> though) choose a path when forking is disabled.
>
>  - Daniel
>
>
> On Fri, Jun 21, 2013 at 12:01 PM, Sunha Ahn <sahn at princeton.edu> wrote:
>
>> 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.
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed