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
