Discussion:
KLEE: ERROR: unable to load symbol(_Stdout) while initializing globals.
Samaneh Navabpour
2013-08-29 18:40:42 UTC
Permalink
Hi,

Im using Klee to generate test cases for libc, but in some cases (such
as getpass.c) Klee gives the following error and terminates before
executing the program:

KLEE: ERROR: unable to load symbol(_Stdout) while initializing globals.


I wrote a simple program:

#include<stdio.h>

int main(int argc, char ** argv)
{
fprintf(stdout, "Hello World \n");
return 0;
}


and Klee still gives the error. Note that the parameters used by
stdout are not symbolized. Im sensing that Klee has issues with
'stdout'.

When I replace 'stdout' with 'stderr', then Klee gives the following error:

KLEE: ERROR: unable to load symbol(_Stderr) while initializing globals.

I dont understand what's going wrong. Can someone explain the reason
of the error and how I can overcome it so I can generate test cases
for libc programs that use stdout and stderr.

Thanks
Samaneh
--
Samaneh Navabpour
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada, N2L 3G1
Cristian Cadar
2013-08-30 15:23:10 UTC
Permalink
Hi Samaneh, I don't have any problems running your example. You need to
provide more information about your setup. The best thing would be to
do so by filling a bug report on github.

I assume you also fail tests in the regression suite?

Best,
Cristian
Post by Samaneh Navabpour
Hi,
Im using Klee to generate test cases for libc, but in some cases (such
as getpass.c) Klee gives the following error and terminates before
KLEE: ERROR: unable to load symbol(_Stdout) while initializing globals.
#include<stdio.h>
int main(int argc, char ** argv)
{
fprintf(stdout, "Hello World \n");
return 0;
}
and Klee still gives the error. Note that the parameters used by stdout
are not symbolized. Im sensing that Klee has issues with 'stdout'.
KLEE: ERROR: unable to load symbol(_Stderr) while initializing globals.
I dont understand what's going wrong. Can someone explain the reason of
the error and how I can overcome it so I can generate test cases for
libc programs that use stdout and stderr.
Thanks
Samaneh
Loading...