I think that's because llvm compiler actually decompose this compound conditional expression into two different branches. If you check generated klee-last/assembly.ll file, you will find there are 4 br instructions, two of them are unconditional. and the control flow graph has exactly 3 paths. klee just interprets llvm. If you can control the way in that llvm generate these instructions, then klee's behavior will be changed. but, i don't think it's generally doable. And, try -optimize option on klee, you will get one path.
Chaoqiang On Fri, Jan 27, 2012 at 1:30 AM, Paul Thomson <[email protected]> wrote: > 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 >
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
