The short answer is that KLEE can call external functions with symbolic
arguments. Use the --allow-external-sym-calls flag as in
klee.cde --libc=uclibc --posix-runtime --init-env --allow-external-sym-calls
./test2.o --sym-arg 2 10 10
However, this will not give the result you expect. If a function is 'external',
it's executed natively so it cannot return a symbolic value. Easiest fix here
is to recompile uclibc with printf via
make KLEE_CFLAGS="-DKLEE_SYM_PRINTF"
Paul
On 9 Jun 2011, at 17:35, Henning Femmer wrote:
> 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");
> }
> }
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110611/7e2933c8/attachment-0001.html
