[klee-dev] Symbolic calls to mqueue.h functions ?

[Nowack, Martin]

Hi,

> On 24. Apr 2023, at 10:53, LONGUET Delphine <delphine.longuet at 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