Hi, I'm playing around with KLEE recently. I followed the document "Building KLEE (LLVM 3.4)" and successfully run all the examples in KLEE.
However, when I wanted to run my own program using KLEE, some errors occurred. (See the following console output) [Command:] klee -load=/usr/lib/x86_64-linux-gnu/libssl.so --libc=uclibc --posix-runtime -emit-all-errors -allow-external-sym-calls klee_client.bc [Console output:] KLEE: NOTE: Using klee-uclibc : /home/testuser/Downloads/klee/Release+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/testuser/Downloads/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/testuser/Downloads/klee_test/klee-out-3" KLEE: WARNING ONCE: function "__libc_connect" has inline asm KLEE: WARNING ONCE: function "setsockopt" has inline asm KLEE: WARNING ONCE: function "shutdown" has inline asm KLEE: WARNING ONCE: function "socket" has inline asm KLEE: WARNING ONCE: function "__libc_recvfrom" has inline asm KLEE: WARNING ONCE: function "__libc_sendto" has inline asm KLEE: WARNING: undefined reference to function: ERR_clear_error KLEE: WARNING: undefined reference to function: ERR_error_string KLEE: WARNING: undefined reference to function: ERR_get_error KLEE: WARNING: undefined reference to function: OPENSSL_config KLEE: WARNING: undefined reference to function: SSL_CTX_ctrl KLEE: WARNING: undefined reference to function: SSL_CTX_free KLEE: WARNING: undefined reference to function: SSL_CTX_new KLEE: WARNING: undefined reference to function: SSL_CTX_set_next_proto_select_cb KLEE: WARNING: undefined reference to function: SSL_connect KLEE: WARNING: undefined reference to function: SSL_free KLEE: WARNING: undefined reference to function: SSL_get_error KLEE: WARNING: undefined reference to function: SSL_library_init KLEE: WARNING: undefined reference to function: SSL_load_error_strings KLEE: WARNING: undefined reference to function: SSL_new KLEE: WARNING: undefined reference to function: SSL_read KLEE: WARNING: undefined reference to function: SSL_set_fd KLEE: WARNING: undefined reference to function: SSL_shutdown KLEE: WARNING: undefined reference to function: SSL_write KLEE: WARNING: undefined reference to function: SSLv23_client_method KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex ... KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 40876048) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: __syscall_rt_sigaction: silently ignoring KLEE: WARNING ONCE: calling external: OPENSSL_config(0) KLEE: WARNING ONCE: calling external: SSL_load_error_strings() KLEE: WARNING ONCE: calling external: SSL_library_init() KLEE: WARNING ONCE: calling external: printf(35435072, 46338336) KLEE: ERROR: /home/testuser/Downloads/klee-uclibc/libc/inet/socketcalls.c:362: inline assembly is unsupported KLEE: done: total instructions = 99493 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 My question is why there are errors in uclibc? Because I compiled it as what the document said, and I didn't find any options (e.g. no-asm) when "configure" uclibc before compiling. Besides, I also noticed that there were many warnings about "undefined reference to function: ...". Should I compile the corresponding libraries to llvm bitcode rather than using existing shared objects? Thanks! Shengtuo Hu
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
