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

[Gleb Popov]

On Tue, Oct 29, 2019 at 10:05 PM Cadar, Cristian <c.cadar at imperial.ac.uk>
wrote:

> 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
>

Thanks for pointers. However, some debugging brought me to a strange loop
in klee::linkModules() function of Module/ModuleUtils.cpp:

while (true) {
  ...
  bool merged = false;
  for (auto &module : modules) {
     ...
     linkTwoModules(composite.get(), std::move(module), errorMsg));
  }
  ...
}

If I understand it right, it exits the loop only when there are no
undefined symbols left, but I don't see how linking the same set of modules
over and over again can help if we actually have some missing symbol.

What am I missing there?


> 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
> >
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed