The problem is that your program registers an exit handler (KLEE: WARNING ONCE: calling external: __cxa_atexit(22093072, 0, 23373792)). When klee exits, this is called and crashes since the function pointer passed is not a ‘real' function pointer.
The atexit call is generated because you have global objects which need to be destroyed (they come from iostream). You can work around the problem by using stdio.h/printf. Paul On 21 Oct 2014, at 20:42, Bin Lin <[email protected]> wrote: > Sorry, I miss part of them. > > (gdb) bt > #0 0x0000000001511d10 in ?? () > #1 0x00002aaaab94b071 in __run_exit_handlers (status=0, listp=0x2aaaabcd06a8 > <__exit_funcs>, run_list_atexit=run_list_atexit@entry=true) > at exit.c:77 > #2 0x00002aaaab94b0f5 in __GI_exit (status=<optimized out>) at exit.c:99 > #3 0x00002aaaab930dec in __libc_start_main (main=0x55a720 <main(int, char**, > char**)>, argc=2, ubp_av=0x7fffffffe4b8, init=<optimized out>, > fini=<optimized out>, rtld_fini=<optimized out>, > stack_end=0x7fffffffe4a8) at libc-start.c:294 > #4 0x00000000005684af in _start () > > > On Tue, Oct 21, 2014 at 12:15 PM, Bin Lin <[email protected]> wrote: > Thanks. > > The LLVM version is 2.9. STP is the recommended version on the homepage of > KLEE. The compiler I used to build the LLVM bitcode is llvm-gcc / llvm-g++ > (the behavior is the same), which is also downloaded following the > instruction on the homepage. I used Release+Asserts to build. The > architecture is x86 and OS is Ubuntu 13.10 > > The backtrace in GDB is as follows. And the source file is attached. Thank > you so much. > > GNU gdb (GDB) 7.6.1-ubuntu > Copyright (C) 2013 Free Software Foundation, Inc. > License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> > This is free software: you are free to change and redistribute it. > There is NO WARRANTY, to the extent permitted by law. Type "show copying" > and "show warranty" for details. > This GDB was configured as "x86_64-linux-gnu". > For bug reporting instructions, please see: > <http://www.gnu.org/software/gdb/bugs/>... > Reading symbols from > /home/blin/Documents/projects/linbin-sefsystemc/klee/src/klee/Release+Asserts/bin/klee...done. > (gdb) r virtual.bc > Starting program: > /home/blin/Documents/projects/linbin-sefsystemc/klee/src/examples/virtualF/../../klee/Release+Asserts/bin/klee > virtual.bc > [Thread debugging using libthread_db enabled] > Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1". > KLEE: output directory is > "/home/blin/Documents/projects/linbin-sefsystemc/klee/src/examples/virtualF/klee-out-1" > KLEE: WARNING: undefined reference to function: _ZNSolsEi > KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev > KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev > KLEE: WARNING: undefined reference to variable: _ZSt4cout > KLEE: WARNING: undefined reference to function: > _ZStlsISt11char_traitsIcEERSt13basic_ostreamIcT_ES5_PKc > KLEE: WARNING: undefined reference to function: __cxa_atexit > KLEE: WARNING: undefined reference to variable: __dso_handle > KLEE: WARNING: undefined reference to function: pthread_cancel > KLEE: WARNING: undefined reference to function: pthread_create > KLEE: WARNING: undefined reference to function: pthread_getspecific > KLEE: WARNING: undefined reference to function: pthread_key_create > KLEE: WARNING: undefined reference to function: pthread_key_delete > KLEE: WARNING: undefined reference to function: pthread_mutex_init > KLEE: WARNING: undefined reference to function: pthread_mutex_lock > KLEE: WARNING: undefined reference to function: pthread_mutex_trylock > KLEE: WARNING: undefined reference to function: pthread_mutex_unlock > KLEE: WARNING: undefined reference to function: pthread_mutexattr_destroy > KLEE: WARNING: undefined reference to function: pthread_mutexattr_init > KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype > KLEE: WARNING: undefined reference to function: pthread_once > KLEE: WARNING: undefined reference to function: pthread_setspecific > KLEE: WARNING ONCE: calling external: _ZNSt8ios_base4InitC1Ev(23373264) > KLEE: WARNING ONCE: calling external: __cxa_atexit(22093072, 0, 23373792) > KLEE: WARNING ONCE: calling external: > _ZStlsISt11char_traitsIcEERSt13basic_ostreamIcT_ES5_PKc(23374656, 23375824) > KLEE: WARNING ONCE: calling external: _ZNSolsEi(23374656, 2) > b1->f() = 2 > b2.f() = 2 > b3.f() = 1 > > KLEE: done: total instructions = 123 > KLEE: done: completed paths = 1 > KLEE: done: generated tests = 1 > > Program received signal SIGSEGV, Segmentation fault. > 0x0000000001511d10 in ?? () > (gdb) c > Continuing. > 0 klee 0x0000000000d66f4f > 1 klee 0x0000000000d67459 > 2 libpthread.so.0 0x00002aaaaacdfbb0 > 3 libpthread.so.0 0x0000000001511d10 > > Program received signal SIGSEGV, Segmentation fault. > 0x0000000001511d10 in ?? () > (gdb) > > > On Tue, Oct 21, 2014 at 2:21 AM, Daniel Liew <[email protected]> > wrote: > > Does anyone have any idea what is going on? BTW, I didn't use any stuff > > related to pthread. Thanks a lot. > > Nobody will be able to help because you have given no where near > enough information to deduce the problem. > > - Include the "simple C++ program" source code (either as an > attachment or on something like Pastebin or Gist) > - Tell us the LLVM version you built KLEE against > - Tell us the STP version you built KLEE against > - Tell us the compiler you used to build the LLVM bitcode > - Tell us what build mode you used (e.g. Debug+Asserts, Release, ... etc) > - Tell us the architecture and OS you are running on (e.g. Ubuntu 14.04 i686) > - Give a proper backtrace by running KLEE in GDB > > > BTW, I didn't use any stuff related to pthread > > Yes but LLVM does. > > > _______________________________________________ > 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
