Hi all, I am not sure if this would be a bug in KLEE - it calls an external longjmp and then a segmentation fault happens. I ran KLEE on Flex like so:
$ klee -max-time=30 -libc=uclibc --posix-runtime flex.bc KLEE: NOTE: Using klee-uclibc : /usr/lib/klee/runtime/klee-uclibc.bca KLEE: NOTE: Using model: /usr/lib/klee/runtime/libkleeRuntimePOSIX.bca KLEE: output directory is "/tmp/buildd/tmp.Wglxl0hoY7/usr/bin/klee-out-0" Using STP solver backend KLEE: WARNING: undefined reference to function: __ctype_b_loc KLEE: WARNING: undefined reference to function: __isoc99_sscanf KLEE: WARNING: undefined reference to function: bindtextdomain KLEE: WARNING: undefined reference to function: gettext KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex KLEE: WARNING: undefined reference to function: log10 KLEE: WARNING: undefined reference to function: longjmp KLEE: WARNING: undefined reference to function: textdomain KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 96231968) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: calling external: textdomain(94078832) KLEE: WARNING ONCE: calling external: bindtextdomain(94078832, 94090144) KLEE: WARNING ONCE: _setjmp: ignoring KLEE: WARNING ONCE: calling external: __ctype_b_loc() KLEE: WARNING ONCE: calling external: gettext(95801488) <stdin>:1: premature EOF KLEE: WARNING: pipe: ignoring (ENFILE) flex.bc: pipe failed KLEE: WARNING: unlink: ignoring (EPERM) flex.bc: error deleting output file lex.yy.c KLEE: WARNING ONCE: calling external: longjmp(94083408, 2) /tmp/hooks/B10-run-klee: line 33: 14600 Segmentation fault klee -max-time=30 -libc=uclibc --posix-runtime $(basename $f).bc The .bc file flex.bc is available from: http://soarlab.org/files/klee/sut/flex-2.5.39/flex.bc -- Regards, Marko Dimjašević <ma...@cs.utah.edu> . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev