What command line arguments are you running it with?
Suhabe
On Tue, May 25, 2010 at 3:13 PM, Seungbeom Kim <sbkim at stanford.edu> wrote:
> 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
>
