Hi,
I find that #include <iostream> alone causes KLEE to segfault
at the end of the run, but not with --libc=klee or --libc=uclibc.
$ cat header.cc
#include <iostream>
int main(int, char**)
{
}
$ klee --libc=none header.o
...
KLEE: done: total instructions = 39
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
0 klee 0x089896a8
Segmentation fault (core dumped)
$ klee --libc=uclibc header.o
...
KLEE: done: total instructions = 11118
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
Why does this happen? I suspect this has to do with the initialization
of the standard stream objects (std::cout, etc.), but the klee libc
or uclibc doesn't have anything to do with the C++ standard library,
does it?
(Anyway, segfault means a bug in klee that should be fixed. =D)
The following program:
#include <ostream>
#include <iostream>
int main(int, char**)
{
std::cout << "Hello, world!\n";
}
runs fine with any of the --libc={none,klee,uclibc} options, i.e.
prints the string on the terminal successfully, though --libc=none
causes the same segfault at the end of the run. This seems to imply
that std::cout is somewhere defined and initialized, but I cannot
see where or how.
Thanks in advance for any ideas or comments.
--
Seungbeom Kim
