Hello Lionel, You are unlikely to be able to run httpd out-of-the-box with only ad-hoc changes. The assertion that you're seeing is probably due to inline assembly. Even if you get rid of that, you're going to stumble across other problems related to the 'undefined' functions that you're getting warnings about. What you can try is to rewrite the functions with inline assembly to C and then use a model which implements the functions used by httpd. You might have a shot with cloud9 (https://cloud9.epfl.ch) but I can't say more because I didn't use it.
Paul On 10 May 2012, at 13:58, Lionel PRAT wrote: > Hello, > I modified lib / Module / IntrinsicCleaner.cpp in klee. At line 163 I > commented: > "/ / ii-> eraseFromParent ();" > Since the code goes but now I get a new problem ... Do you think this > is due to my change? > here is the error: > > klee --posix-runtime --libc=uclibc httpd.bc > KLEE: NOTE: Using model: > /home/dev/klee2/Release+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: output directory = "klee-out-9" > WARNING: this target does not support the llvm.stacksave intrinsic. > KLEE: WARNING: function "impl_pollset_create4612" has inline asm > KLEE: WARNING: function "__libc_accept" has inline asm > KLEE: WARNING: function "bind" has inline asm > KLEE: WARNING: function "__libc_connect" has inline asm > KLEE: WARNING: function "getpeername" has inline asm > KLEE: WARNING: function "shmget" has inline asm > KLEE: WARNING: function "getsockname" has inline asm > KLEE: WARNING: function "getsockopt" has inline asm > KLEE: WARNING: function "listen" has inline asm > KLEE: WARNING: function "__libc_recvfrom" has inline asm > KLEE: WARNING: function "__semctl" has inline asm > KLEE: WARNING: function "semget" has inline asm > KLEE: WARNING: function "semop" has inline asm > KLEE: WARNING: function "__libc_sendto" has inline asm > KLEE: WARNING: function "setsockopt" has inline asm > KLEE: WARNING: function "shmat" has inline asm > KLEE: WARNING: function "__libc_shmctl" has inline asm > KLEE: WARNING: function "shmdt" has inline asm > KLEE: WARNING: function "shutdown" has inline asm > KLEE: WARNING: function "socket" has inline asm > KLEE: WARNING: undefined reference to function: __ctype_b_loc > KLEE: WARNING: undefined reference to function: __isinf > KLEE: WARNING: undefined reference to function: __xstat64 > KLEE: WARNING: undefined reference to function: accept4 > KLEE: WARNING: undefined reference to function: crypt_r > KLEE: WARNING: undefined reference to function: dlclose > KLEE: WARNING: undefined reference to function: dlerror > KLEE: WARNING: undefined reference to function: dlopen > KLEE: WARNING: undefined reference to function: dlsym > KLEE: WARNING: undefined reference to function: dup3 > KLEE: WARNING: undefined reference to function: epoll_create1 > KLEE: WARNING: undefined reference to function: epoll_ctl > KLEE: WARNING: undefined reference to function: epoll_wait > KLEE: WARNING: undefined reference to function: flock > KLEE: WARNING: undefined reference to function: freeifaddrs > KLEE: WARNING: undefined reference to function: getdomainname > KLEE: WARNING: undefined reference to function: getifaddrs > KLEE: WARNING: undefined reference to function: getpgid > KLEE: WARNING: undefined reference to function: iconv > KLEE: WARNING: undefined reference to function: iconv_close > KLEE: WARNING: undefined reference to function: iconv_open > KLEE: WARNING: undefined reference to function: klee_get_valuel > KLEE: WARNING: undefined reference to function: llvm.atomic.cmp.swap.i32.p0i32 > KLEE: WARNING: undefined reference to function: llvm.atomic.cmp.swap.i64.p0i64 > KLEE: WARNING: undefined reference to function: llvm.atomic.load.add.i32.p0i32 > KLEE: WARNING: undefined reference to function: llvm.atomic.load.sub.i32.p0i32 > KLEE: WARNING: undefined reference to function: llvm.atomic.swap.i32.p0i32 > KLEE: WARNING: undefined reference to function: llvm.atomic.swap.i64.p0i64 > KLEE: WARNING: undefined reference to function: llvm.dbg.declare > KLEE: WARNING: undefined reference to function: llvm.dbg.value > KLEE: WARNING: undefined reference to function: llvm.memory.barrier > KLEE: WARNING: undefined reference to function: modf > KLEE: WARNING: undefined reference to function: poll > KLEE: WARNING: undefined reference to function: prctl > KLEE: WARNING: undefined reference to function: pthread_attr_destroy > KLEE: WARNING: undefined reference to function: pthread_attr_getdetachstate > KLEE: WARNING: undefined reference to function: pthread_attr_init > KLEE: WARNING: undefined reference to function: pthread_attr_setdetachstate > KLEE: WARNING: undefined reference to function: pthread_attr_setguardsize > KLEE: WARNING: undefined reference to function: pthread_attr_setstacksize > KLEE: WARNING: undefined reference to function: pthread_cond_broadcast > KLEE: WARNING: undefined reference to function: pthread_cond_destroy > KLEE: WARNING: undefined reference to function: pthread_cond_init > KLEE: WARNING: undefined reference to function: pthread_cond_signal > KLEE: WARNING: undefined reference to function: pthread_cond_timedwait > KLEE: WARNING: undefined reference to function: pthread_cond_wait > KLEE: WARNING: undefined reference to function: pthread_create > KLEE: WARNING: undefined reference to function: pthread_detach > KLEE: WARNING: undefined reference to function: pthread_equal > KLEE: WARNING: undefined reference to function: pthread_exit > KLEE: WARNING: undefined reference to function: pthread_getspecific > KLEE: WARNING: undefined reference to function: pthread_join > 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_kill > KLEE: WARNING: undefined reference to function: pthread_mutex_consistent_np > KLEE: WARNING: undefined reference to function: pthread_mutex_destroy > 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_setprotocol > KLEE: WARNING: undefined reference to function: pthread_mutexattr_setpshared > KLEE: WARNING: undefined reference to function: pthread_mutexattr_setrobust_np > KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype > KLEE: WARNING: undefined reference to function: pthread_once > KLEE: WARNING: undefined reference to function: pthread_rwlock_destroy > KLEE: WARNING: undefined reference to function: pthread_rwlock_init > KLEE: WARNING: undefined reference to function: pthread_rwlock_rdlock > KLEE: WARNING: undefined reference to function: pthread_rwlock_tryrdlock > KLEE: WARNING: undefined reference to function: pthread_rwlock_trywrlock > KLEE: WARNING: undefined reference to function: pthread_rwlock_unlock > KLEE: WARNING: undefined reference to function: pthread_rwlock_wrlock > KLEE: WARNING: undefined reference to function: pthread_self > KLEE: WARNING: undefined reference to function: pthread_setspecific > KLEE: WARNING: undefined reference to function: pthread_sigmask > KLEE: WARNING: undefined reference to function: pthread_yield > KLEE: WARNING: undefined reference to function: sem_close > KLEE: WARNING: undefined reference to function: sem_open > KLEE: WARNING: undefined reference to function: sem_post > KLEE: WARNING: undefined reference to function: sem_trywait > KLEE: WARNING: undefined reference to function: sem_unlink > KLEE: WARNING: undefined reference to function: sem_wait > KLEE: WARNING: undefined reference to function: sendfile > KLEE: WARNING: undefined reference to function: sigwaitinfo > KLEE: WARNING: undefined reference to function: strerror_r > KLEE: WARNING: undefined reference to variable: sys_siglist > KLEE: WARNING: undefined reference to function: writev > klee: Executor.cpp:1002: const klee::Cell& > klee::Executor::eval(klee::KInstruction*, unsigned int, > klee::ExecutionState&) const: Assertion `vnumber != -1 && "Invalid > operand to eval(), not a value or constant!"' failed. > 0 klee 0x0000000000d1e8af > 1 klee 0x0000000000d20b12 > 2 libpthread.so.0 0x00007ffe44349ff0 > 3 libc.so.6 0x00007ffe4365b1b5 gsignal + 53 > 4 libc.so.6 0x00007ffe4365dfc0 abort + 384 > 5 libc.so.6 0x00007ffe43654301 __assert_fail + 241 > 6 klee 0x000000000055fce1 > 7 klee 0x0000000000573675 > klee::Executor::executeInstruction(klee::ExecutionState&, > klee::KInstruction*) + 7413 > 8 klee 0x0000000000576d6e > klee::Executor::run(klee::ExecutionState&) + 1774 > 9 klee 0x0000000000577864 > klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, > char**) + 2116 > 10 klee 0x000000000055c53c main + 10748 > 11 libc.so.6 0x00007ffe43647c8d __libc_start_main + 253 > 12 klee 0x00000000005537b9 > Abandon > > > Thx > > Lionel > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
