Thank you for your reply.
I coined another program which is the same as 'islower' program in tutorials 1,
except that the function name is 'abs', rather 'my_islower'. Klee just generate
1 test case which is '0'.
It seems that it is because the function 'abs(int x)' is same as the function
abs(int x) in standard C library.
The program as follows only gets 1 path and 1 test case ( '0' ) from klee.
//*********
int abs(int x) {
if(x < 0)
return -1*x;
else
return x;
}
int main(int argc, char* argv[]) {
int c;
klee_make_symbolic(&c, sizeof(c), "input");
return abs(c);
}
//***********
while the program as follows could get 2 paths and 2 test cases from klee.
//***************
int my_abs(int x) {
if(x < 0)
return -1*x;
else
return x;
}
int main(int argc, char* argv[]) {
int c;
klee_make_symbolic(&c, sizeof(c), "input");
return my_abs(c);
}
//***************
The only difference of these two programs is the function name. But I replace
the function name with 'putchar()' which is another function in C library.
The results is different:
Klee also generates two test case. But the two input are all '0'.
data: '\x00\x00\x00\x80'
and
data: '\x00\x00\x00\x00'
It is both 0 on the little-endian machine.
It seems that the function name brings confusion to klee, is that right?
Best
Yufeng
Paul Marinescu
Re: [klee-dev] ask for help
Most likely the compiler optimizes away the if/then/else (it could for example
transform it into a bitwise operation here). Look at the assembly.ll file
generated in the klee output folder to see what's going on.
Paul
On 14 Jul 2011, at 08:52, Zhang Yufeng wrote:
Hi, everybody. I am new to klee.
Now I have a problem. Klee generates 3 test cases for the islower() function
after exploring 3 paths.
/*islower.c*/
int islower(char c)
{
if(x >= 'a' && x <= 'z') { return 1;}
else {return 0;}
}// end
But why it just explores 1 path and generate 1 test case for function abs()?
The test case is '0'.
/*absolute value of integer*/
int abs(int x) {
if(x < 0)
return -1*x;
else
return x;
}// end
The difference is that the type of the parameter of two functions are
different. Anyone can tell me why?
Thank you very much!
Best.
Yufeng
_______________________________________________
klee-dev mailing list
klee-dev at keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110717/5baf8813/attachment.html
