Hi, > On 24. Apr 2023, at 10:53, LONGUET Delphine > <delphine.long...@thalesgroup.com> wrote: > > > I am trying to execute Klee on a code using mqueue.h and despite the > -posix-runtime and -libc=uclibc options, functions mq_open, mq_close, etc, > remain "undefined references". I can see that there actually are > implementations of these functions in /klee-uclibc/librt/, but they don't > seem to exist in klee-uclibc.bca which is used during the execution of Klee.
With `-libc=uclibc`, only `klee-uclibc/lib/libc.a` is linked/loaded (it’s an archive containing respective bitcode files). Functions like `mq_*` are part of `lib/librt.a`. This library is not loaded which is unfortunately not that obvious. Can you try to link/load the library using `--link-llvm-lib=/path/to/klee-uclibc/lib/librt.a` as an additional argument for KLEE? The library should contain the necessary additional bitcode files. > In a more general way, how can I know what exactly is in klee-uclibc? With `ar t klee-uclibc/lib/libc.a` the files that are part of the library are listed. Their names mirror the source code files. Let me know if that works. Best, Martin _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
