Hi Martin, Thanks a lot for your answer. That works, in the sense that now mq_open is found, but unfortunately, the implementation contains assembly code not supported by Klee :
KLEE: WARNING: function "__syscall_mq_open" has inline asm [...] KLEE: ERROR: librt/mq_open.c:15: inline assembly is unsupported In file librt/mq_open.c (lines 14-15): #define __NR___syscall_mq_open __NR_mq_open static inline _syscall4(int, __syscall_mq_open, const char*, name, int, oflag, __kernel_mode_t, mode, void *, attr); Is there anything I can do about it? Thank you. Best regards, Delphine > -----Message d'origine----- > De : Nowack, Martin <m.now...@imperial.ac.uk> > Envoyé : mardi 25 avril 2023 15:59 > À : LONGUET Delphine <delphine.long...@thalesgroup.com> > Cc : klee-dev <klee-dev@imperial.ac.uk> > Objet : Re: [klee-dev] Symbolic calls to mqueue.h functions ? > > 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
