Hi Oscar, Hongxu,
Thank you for you comment.
Yes, you are right. In practice, my test code have an uninitialized error.
But now I am considering some variables from external environment. These
variables may be uninitialized, so I use pointer p in function 'test' to
describe such a simple situation. I want to use the if-statement at line 2
to judge whether the external pointer p is NULL, if it is I want to
explicitly allocate some space to it at line 3. But now I know KLEE cannot
judge on an uninitialized pointer.
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
On Wed, May 14, 2014 at 10:51 PM, Oscar Soria Dustmann <
Post by Oscar Soria DustmannHi Qiuping,
your code exhibits undefined behaviour as you read from uninitialised
memory. The reason it doesn't fail when run natively is implementation
defined and pure luck. It's not that KLEE needs the initialisation; The
C standard demands it (reason behind it: Stack variables are not
default-initialised for performance reasons).
I'd actually consider it desired behaviour for a testtool to throw you
an error.
Cheers,
Oscar
Post by Qiuping YiHi, Paul
1void test2(int *p) {
2 if (p == NULL)
3 p = malloc(sizeof(*p));
4 *p = 1;
}
5 int main() {
6 int *p;
7 test(p);
8 return 0;
}
This code was executed without any error after compiled with gcc.
However, when
Post by Qiuping YiI applied KLEE to this code, it encountered an 'out of bound pointer'
error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
needs to explicitly initialize each variable, containing the pointers,
right?
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
Post by Paul ThomsonPlease can you provide the code that calls test?
int main()
{
int *p = NULL;
test(p);
return 0;
}
Thanks,
Paul
Post by Qiuping YiHi, everyone
I found a strange behavior of KLEE.
When I applied KLEE to the next code snippet, a out-of-bound-pointer
error happened at line 3. However, this code snippet explicitly
allocates
Post by Qiuping YiPost by Paul ThomsonPost by Qiuping Yispace for pointer p at line 2 when it is evaluated to NULL. So what's
wrong?
Post by Qiuping YiPost by Paul ThomsonPost by Qiuping Yi0 void test (int *p) {
1 if (p == NULL)
2 p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev