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

[Qiuping Yi]

Hi Oscar, Hongxu,

Thank you for you comment.

Yes, you are right. In practice, my test code have an uninitialized error.
But now I am considering some variables from external environment. These
variables may be uninitialized, so I use pointer p in function 'test' to
describe such a simple situation. I want to use the if-statement at line 2
to judge whether the external pointer p is NULL, if it is I want to
explicitly allocate some space to it at line 3. But now I know KLEE cannot
judge on an uninitialized pointer.



--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Wed, May 14, 2014 at 10:51 PM, Oscar Soria Dustmann <
Oscar.SoriaDustmann at comsys.rwth-aachen.de> wrote:

> 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
> >
>
> _______________________________________________
> 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