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 <[email protected]> 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 <[email protected]> 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
>>> [email protected]
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> [email protected]
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
>
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
