[klee-dev] libc function "open" is defined in POSIX runtime

Cadar, Cristian c.cadar at imperial.ac.uk
Tue Oct 29 18:05:25 GMT 2019


Hi Gleb,

We applied various changes to uclibc to make it work with KLEE, so I 
think taking a look at those patches would help.  I don't recall the 
details, but based on a quick search, I think this patch might be 
relevant: 
https://github.com/klee/klee-uclibc/commit/7231f48dd8e2f9f15f721a77639d7eeea6efd38f

This PR from Martin might also be useful:
https://github.com/klee/klee/pull/483
Look in particular at linkWithMusllibc()

I would welcome changes to KLEE to make it easier to plug in other libc 
implementations.

Best,
Cristian

On 26/10/2019 18:50, Gleb Popov wrote:
> Hello.
> 
> I'm trying to make KLEE support FreeBSD libc instead of uclibc. When I 
> run KLEE with my libc.bca, I get the following error:
> 
> error: Linking globals named 'open': symbol multiply defined!
> 
> It turned out that POSIX runtime contains definition of "open" function, 
> as well as FreeBSD libc do. How to handle this properly?
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 


More information about the klee-dev mailing list