[klee-dev] segFault
Paul Marinescu
paul.marinescu at imperial.ac.uk
Tue Oct 21 23:16:29 BST 2014
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 <linbinmr at gmail.com> 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 at 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 <linbinmr at gmail.com> 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 <daniel.liew at imperial.ac.uk> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list