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

[LONGUET Delphine]

Hello,

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.

#include <klee/klee.h>
#include <fcntl.h>
#include <mqueue.h>

int main() {
  mqd_t mq;
  char name[5];
  klee_make_symbolic(name, sizeof(name), "name");

  mq = mq_open(name, O_RDWR | O_CREAT, 0700, NULL);

  if(mq == -1) {
    return 1;
  }
  return 0;
}

$ clang -c -g -I ~/klee/include -emit-llvm queue.c 
$ klee -posix-runtime -libc=uclibc queue.bc
KLEE: NOTE: Using POSIX model: /home/user/klee_deps/klee_build110stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc: /home/user/klee_deps/klee_build110stp_z3/runtime/lib/klee-uclibc.bca
[...]
KLEE: WARNING: undefined reference to function: mq_open [...]
KLEE: WARNING ONCE: calling external: mq_open(93983045383648, 66, 448, 0) at queue.c [...]
KLEE: done: completed paths = 1

Is there something I am doing wrong? How can I link to the Klee implementation of function mq_open?
In a more general way, how can I know what exactly is in klee-uclibc?

Thank you very much for your help.

Best regards,
Delphine Longuet