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