Hello!
I was very excited by your papers and started using KLEE. I was able to use and
create some smaller examples with the "self-contained package" and could also
execute the coreutils example.
Now I tried to apply KLEE on a different example that uses external functions.
From the paper I understood that using uclibc or klee-lib, I could call these
functions symbolically. However, from the output I assume that the function
(here printf) is not properly called or discovered.
Is KLEE able to handle these functions, and if so, what did I do wrong?
I attached the console output and my program.
The program prints an integer value and checks the return value of printf, that
should usually be the number of chars written. I expected it to create two
different test cases.
Thank you very much for your help,
Henning
llvm-gcc.cde -I../../include/ --emit-llvm -c -g test2.c
klee.cde --libc=uclibc --posix-runtime --init-env ./test2.o --sym-arg 2 10 10
KLEE: NOTE: Using model:
/home/pgbovine/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-86"
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: syscall(54, 0, 21505, 35203120)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: ERROR: /home/pgbovine/klee/examples/test/test2.c:12: external call with
symbolic argument: printf
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 10537
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
The program:
#include <stdio.h>
#include "klee/klee.h"
int main(int cArgs, char* args[])
{
int n;
int j;
klee_make_symbolic(&n, sizeof(int), "n");
klee_make_symbolic(&j, sizeof(int), "j");
n = printf("Value: %d",j);
if(n>50)
{
printf("big\n");
}
else
{
printf("small\n");
}
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110609/3c9b53fe/attachment.html
