Re: [klee-dev] Strange behavior of KLEE when evaluating NULL pointer
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 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) {
> 1if (p == NULL)
> 2p = malloc(sizeof(*p));
>
> 3 *p = 2;
> }
>
> Best Regards!
>
>
> Qiuping Yi
> Institute Of Software
> Chinese Academy of Sciences
>
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Strange behavior of KLEE when evaluating NULL pointer
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) {
1if (p == NULL)
2p = malloc(sizeof(*p));
3 *p = 2;
}
Best Regards!
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] ?????? ?????? Full Name of KLEE
Hope for help. Thanks everyone -- -- ??: ""; : 2014??5??13??(??) 5:07 ??: "K Kylin"; "klee-dev"; : [klee-dev] ?? Full Name of KLEE Hi, I have run an example using KLEE. Many files are generated in klee-out-x. In http://klee.github.io/klee/ , some information accounting for these files are offered, but are far from enough. So i want to know what the information in these files exactly mean. Have you known some detailed introduction about those files? Thanks. Zeng Jie -- -- ??: "K Kylin"; : 2014??5??13??(??) 1:14 ??: "klee-dev"; : [klee-dev] Full Name of KLEE Hi,I read papers about KLEE, but I didn't find the full name of KLEE. So what's the full name of KLEE, or is KLEE not an abbreviation?? Thanks. Kylin___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] ?????? Full Name of KLEE
Hi, I have run an example using KLEE. Many files are generated in klee-out-x. In http://klee.github.io/klee/ , some information accounting for these files are offered, but are far from enough. So i want to know what the information in these files exactly mean. Have you known some detailed introduction about those files? Thanks. Zeng Jie -- -- ??: "K Kylin"; : 2014??5??13??(??) 1:14 ??: "klee-dev"; : [klee-dev] Full Name of KLEE Hi,I read papers about KLEE, but I didn't find the full name of KLEE. So what's the full name of KLEE, or is KLEE not an abbreviation?? Thanks. Kylin___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
