Unknown
2011-01-03 16:35:13 UTC
Dear all,
I would like to apply KLEE to test the newest version of Busybox. However, I
failed to execute
busybox.bc because
$ ./busybox ls
LLVM ERROR: Program used external function 'test_main' which could not be
resolved!
test_main, an entry function of 'test' applet in Busybox, could not be
resolved. I checked .config
and found CONFIG_TEST=y, so test_main should be included in the busybox
binary.
Also, I failed to run busybox with KLEE
$ klee ./busybox_unstripped.bc
KLEE: output directory = "klee-out-6"
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: WARNING: function "lbb_prepare" has inline asm
KLEE: WARNING: function "sendmail_main" has inline asm
... SO MANY WARNINGS ...
KLEE: ERROR: unable to load symbol(opt_complementary) while initializing
globals.
sendmail_main, lbb_prepare, and opt_complementary should be included
busybox_unstripped.bc
because they are implemented in Busybox, compiled by llvm-gcc, and linked
with Busybox LLVM bitcode binary.
I use the following command to build busybox
$ make V=1 CC=klee-gcc LD="klee-gcc -Wl," SKIP_STRIP=y
CFLAGS=-fnested-functions
I use LLVM 2.7 and corresponding llvm-gcc version.
I guess the llvm linker llvm-ld may not work correctly due to my mis-use or
unknown reasons.
Do you have experienced applying KLEE to a recent Busybox version?
--
Best Regards
---------------------------------------------
Yunho Kim, Ph.D candidate
Rm# 2438 CS Dept. KAIST
373-1 Guseong-dong, Yuseong-gu
Daejon, South Korea (305-701)
Phone:+82-42-350-7743
Fax:+82-42-350-3510
---------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110104/eb920363/attachment.html
I would like to apply KLEE to test the newest version of Busybox. However, I
failed to execute
busybox.bc because
$ ./busybox ls
LLVM ERROR: Program used external function 'test_main' which could not be
resolved!
test_main, an entry function of 'test' applet in Busybox, could not be
resolved. I checked .config
and found CONFIG_TEST=y, so test_main should be included in the busybox
binary.
Also, I failed to run busybox with KLEE
$ klee ./busybox_unstripped.bc
KLEE: output directory = "klee-out-6"
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: WARNING: function "lbb_prepare" has inline asm
KLEE: WARNING: function "sendmail_main" has inline asm
... SO MANY WARNINGS ...
KLEE: ERROR: unable to load symbol(opt_complementary) while initializing
globals.
sendmail_main, lbb_prepare, and opt_complementary should be included
busybox_unstripped.bc
because they are implemented in Busybox, compiled by llvm-gcc, and linked
with Busybox LLVM bitcode binary.
I use the following command to build busybox
$ make V=1 CC=klee-gcc LD="klee-gcc -Wl," SKIP_STRIP=y
CFLAGS=-fnested-functions
I use LLVM 2.7 and corresponding llvm-gcc version.
I guess the llvm linker llvm-ld may not work correctly due to my mis-use or
unknown reasons.
Do you have experienced applying KLEE to a recent Busybox version?
--
Best Regards
---------------------------------------------
Yunho Kim, Ph.D candidate
Rm# 2438 CS Dept. KAIST
373-1 Guseong-dong, Yuseong-gu
Daejon, South Korea (305-701)
Phone:+82-42-350-7743
Fax:+82-42-350-3510
---------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110104/eb920363/attachment.html