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.
Post by Bin LinSorry, I miss part of them.
(gdb) bt
#0 0x0000000001511d10 in ?? ()
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 ()
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".
<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)
Post by Bin LinDoes 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
Post by Bin LinBTW, I didn't use any stuff related to pthread
Yes but LLVM does.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev