Hi again, On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote:
> Earlier on this list there was a thread on what would be alternatives > to > KLEE-uClibc as the library implementation got rather old, which is > true > for its upstream as well, though to a lesser extent. Here I would like > to ask how to add support for another C library implementation to > KLEE. I started implementing support for the Musl C library in KLEE: https://github.com/mdimjasevic/klee/commit/367543b6 I'd like to use Musl in conjunction with the POSIX runtime. However, when I run KLEE like this: $ klee -libc=musl -posix-runtime hostname.bc I get the following: KLEE: NOTE: Using musl : /home/marko/research/klee/Release +Asserts/lib/musl.bca KLEE: NOTE: Using model: /home/marko/research/klee/Release +Asserts/lib/libkleeRuntimePOSIX.bca KLEE: ERROR: Link with library /home/marko/research/klee/Release +Asserts/lib/libkleeRuntimePOSIX.bca failed: Linking globals named 'access': symbol multiply defined! I haven't been able to track this down. Is this to say that libkleeRuntimePOSIX.bca has a model for the 'access' function and that this clashes with the definition of the 'access' function in Musl? How to avoid multiple symbol definitions? If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version of the library in KLEE (that's what the -libc=musl parameter fetches). -- 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
