Hi all,
I recently noticed that whenever an external syscall() function is invoked
in Klee, the syscall number (the first parameter of the function) is
wrongfully displayed, although the correct syscall actually gets executed. I
studied the external call logging code in the Executor to see if there is
any bug, but I could not find any flaw.
For instance, for the following simple program:
#include <stdio.h>
#include <string.h>
int main(int argc, char **argv) {
int a = 1;
int b = 2;
char buff[256];
sprintf(buff, "Hey there %d, %d!\n", a, b);
write(1, buff, strlen(buff));
return 0;
}
Klee gives the following output (syscall numbers are in bold):
*$ klee --posix-runtime --libc=uclibc --all-external-warnings test.o*
KLEE: NOTE: Using model:
/home/stefan/klee-vanilla/Release/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-1"
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: WARNING: calling external: syscall(*16*, 0, 21505, 28322480)
KLEE: WARNING: calling external: syscall(*16*, 1, 21505, 23118944)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: syscall(*4*, 28261456, 28343024)
KLEE: WARNING: calling external: syscall(*1*, 1, 28458064, 16)
Hey there 1, 2!
KLEE: done: total instructions = 15504
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
While they appear as normal syscall numbers, they are actually incorrect,
according to the Linux syscall table[1] . For instance, the write() syscall
is shown as syscall #1, while it should have been #4. The fstat() syscalls
in the beginning also have the wrong numbers.
Do you have any idea for why this happens? Am I interpreting the output
incorrectly?
Thanks,
Stefan
[1] http://syscalls.kernelgrok.com/
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110420/4249b9b2/attachment.html
