[klee-dev] Adding support for another C library

[Marko Dimjašević]

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ć <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20161015/73593618/attachment.sig>