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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
