Thanks! it helped a lot! Best regards, Sunha.
2013/6/21 David Ramos <[email protected]> > Yes. Otherwise, it would be exploring infeasible paths, which would be > unsound and could generate false positives. > > On Jun 21, 2013, at 1:39 PM, Sunha Ahn <[email protected]> wrote: > > 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
