My apologies; I meant to reply on the mailing list, but I replied directly.
Sorry,
Brady J. Garvin
Seungbeom Kim,
I'm no expert on KLEE, but I would say from the trace that strcmp is being
evaluated by a call to native assembly. In other words, strcmp is not
compiled to LLVM bitcode, so KLEE is approximating the functions behavior
by executing it directly. It's no surprise then that the string it picks
as a concrete argument is not equal to "world".
Presumably you would like to cover both branches. In this case I believe
that you can use uclibc and --posix-runtime as documented in the
tutorials. Or, if necessary, you could also provide a C implementation of
strcmp in your sourcefile.
Like I said, I have only had short experience with KLEE. Others may
correct or improve my response.
Thanks,
Brady J. Garvin
> Hi,
>
> When I run the following simple program with KLEE:
> ------------------------------------------------------------------------
#include <stdlib.h>
> #include <stdio.h>
> #include <string.h>
>
> int main(int argc, char** argv)
> {
> const size_t LEN = 10;
> char *s = malloc(LEN);
> klee_make_symbolic(s, LEN, "s");
>
> if (strcmp(s, "world") != 0)
> puts("different");
> else
> puts("same");
>
> return 0;
> }
> ------------------------------------------------------------------------
>
> I expect to see that both branches are covered and to see at least one
occurrence of "different" and at least one occurrence of "same".
However, the lastest version of KLEE outputs:
> ------------------------------------------------------------------------
KLEE: output directory = "klee-out-0"
> KLEE: WARNING: undefined reference to function: puts
> KLEE: WARNING: undefined reference to function: strcmp
> KLEE: WARNING: calling external: strcmp(146291400, 146271112)
> KLEE: WARNING: calling external: puts(146271424)
> different
>
> KLEE: done: total instructions = 38
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
> ------------------------------------------------------------------------
>
> Is this the expected behaviour, or a bug in KLEE, or a configuration
problem on my side?
>
> Thanks,
>
> --
> Seungbeom Kim
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
