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

[Oscar Soria Dustmann]

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 <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
>>
>>
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>