Very simple:
$ klee-gcc -c -g strcmp.c
$ klee strcmp.o
Oops, it seems that uclibc is not linked by default, contrary to
the older version (before open sourcing) which links it by default.
(I was confused and mistaken when I thought --posix-runtime would
enable it; it is --init-env that is enabled by --posix-runtime. ;))
$ klee --libc=uclibc strcmp.o
solves the problem.
Thanks!
On 2010-05-25 15:40, Suhabe Bugrara wrote:
> 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
--
Seungbeom Kim
