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 < oscar.soriadustm...@comsys.rwth-aachen.de> wrote: > Hi 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 > > On 14/05/14 15:43, Qiuping Yi wrote: > > Hi, Paul > > > > Next is my whole test code: > > > > 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 > > I 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 > > > > > > On Tue, May 13, 2014 at 6:50 PM, Paul Thomson <pault...@gmail.com> > wrote: > > > >> Please can you provide the code that calls test? > >> > >> Or, please try using something like: > >> > >> int main() > >> { > >> int *p = NULL; > >> test(p); > >> return 0; > >> } > >> > >> > >> Thanks, > >> Paul > >> > >> > >> On 13 May 2014 11:09, Qiuping Yi <yiqiup...@gmail.com> wrote: > >> > >>> Hi, 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 > >>> space for pointer p at line 2 when it is evaluated to NULL. So what's > wrong? > >>> > >>> 0 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 > >>> klee-dev@imperial.ac.uk > >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >>> > >>> > >> > >> _______________________________________________ > >> klee-dev mailing list > >> klee-dev@imperial.ac.uk > >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >> > >> > > > > > > > > _______________________________________________ > > klee-dev mailing list > > klee-dev@imperial.ac.uk > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev