Dear KLEE users and devs, I've noticed others had issues with KLEE saying it is unable to load a symbol:
http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000017.html https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01252.html To the former Cristian Cadar replied: "[M]ost likely you have not compiled all libraries used by vim to LLVM bitcode.", where a user was trying to use KLEE on vim. Can someone explain a bit more why this error is happening? I'm trying to analyze Debian packages with KLEE and I ran into the same issue. For example, I see the error when I try to run KLEE on 'vim' compiled from a Debian package. I tried to run KLEE on the apt-sortpkgs utility as well and I get the same kind of error: KLEE: ERROR: unable to load symbol(_config) while initializing globals. Note I build packages from their source, hence whatever libraries a package may have, they will be compiled to LLVM IR and hopefully linked together with WLLVM. I see the error gets reported when KLEE is in lib/Core/Executor.cpp. However, with my current familiarity with KLEE's source code, I'm unable to explain to myself why this happens. I ran it with KLEE 1.2.0 and KLEE-uClibc 1.0.0 with .bc files compiled with LLVM 3.4. Here is how I run KLEE: klee -max-time=30 -libc=uclibc --posix-runtime apt-sortpkgs.bc If needed, I will provide .bc files of programs for which the error is reported. I'd like to understand why this is happening as I'm expecting it might be quite common for many other packages too. -- 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
