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
