Hi, David. Thanks! I got it. May I ask one more question? I guess you mean if one of the branches is not feasible, KLEE will choose the feasible branch then?
Thanks, Sunha. 2013/6/21 David Ramos <[email protected]> > Sunha, > > KLEE only chooses a random branch if both branch targets are feasible. > Your call to klee_assume() constrains the value of 'x' so that only one of > those branch targets is feasible in each of your examples. > > -David > > On Jun 21, 2013, at 1:23 PM, Sunha Ahn <[email protected]> wrote: > > 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 <[email protected]> > >> 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 <[email protected]> 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 >>> [email protected] >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>> >>> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
