Perhaps replace || with | so the if condition is: (x == 1 | (x|1) == 3) Thanks, Paul
Sent from my iPhone On 27 Jan 2012, at 09:18, James Hongyi Zeng <[email protected]> wrote: > Hi all, > > I am new to KLEE. I wish to use KLEE to analyze a branch-intensive > program, where I want to hit every path exactly once, no matter how > complicated the condition statement is. > > I come up with the following example. Where KLEE will produce 3 test > cases - x=0, 1, 2. However, there are only 2 branches. I noticed that if I > replace x|1 with x or x+1, KLEE will ignore it and just use x=1. I guess > that's because of the uncertainty by bitmask. How can I instruct KLEE to hit > the if statement just once in the example below? > > Thanks, > James > > /* > * First KLEE tutorial: testing a small function > */ > > #include <klee/klee.h> > > int my_islower(uint32_t x) { > if (x == 1 || (x|1) == 3) return 0; > return 0; > } > > int main() { > uint32_t c; > klee_make_symbolic(&c, sizeof(c), "input"); > return my_islower(c); > } > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
