[klee-dev] how klee_set_forking works exactly?

[Daniel Dunbar]

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
>
>
-------------- next part --------------
HTML attachment scrubbed and removed