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

[Paul Thomson]

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
>
>
-------------- next part --------------
HTML attachment scrubbed and removed