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
