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

[Qiuping Yi]

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