[klee-dev] Strange behavior of KLEE when evaluating NULL pointer

[Qiuping Yi]

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 <pault543 at 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 <yiqiuping at 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 at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed