Re: [klee-dev] failed external call: fgets

2017-06-19 Thread Dan Liew
On 16 June 2017 at 17:05, Nourah mmm  wrote:
> Hi,
>
> I try to run KLEE on cutcp benchmark from (Parboil Benchmarks). The
> benchmark consists from the following program: main.c  parboil.c readatom.c
> cutcpu.c excl.c output.c
>
> First I compile it with the following command:
> myclang -I /home/klee/klee_src/include -emit-llvm -c -g main.c  parboil.c
> readatom.c cutcpu.c excl.c output.c
>
> Then, I run KLEE with this command:
> myklee --posix-runtime --libc=uclibc  --link-llvm-lib=parboil.bc
> --link-llvm-lib=cutcpu.bc --link-llvm-lib=excl.bc --link-llvm-lib=output.bc
> --link-llvm-lib=readatom.bc ./main.bc -i
> /home/naloboud/parboil/datasets/cutcp/small/input/watbox.sl40.pqr
>
> However I get this error:
> KLEE: NOTE: Using model:
> /home//klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: Linking in library: parboil.bc.
>
> KLEE: Linking in library: cutcpu.bc.
>
> KLEE: Linking in library: excl.bc.
>
> KLEE: Linking in library: output.bc.
>
> KLEE: Linking in library: readatom.bc.

I think the problem is the way you are linking. The `--link-llvm-lib`
flag links after klee-uclibc links in. The code that is failing
probably comes from `readatom.bc`.

This code is calling `fgets()` but because klee-uclibc has already
been linked in (note we do "static style" linking so only the parts of
klee-uclibc that are needs get linked in)
it's too late to get a definition.

Arguably this a bug in the `--link-llvm-lib` flag but I'm not
particularly interested in fixing it because I voted against adding
this feature when it was first introduced.

What I'd recommend doing is using wllvm
(https://github.com/travitch/whole-program-llvm) to build your program
and tell the build system to link everything statically.
If you do this everything should be linked together properly.

Alternatively if you know which `bc` files you want to link together
just use the `llvm-link` tool to link them all together before you
give them to KLEE.

HTH,
Dan.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] failed external call: fgets

2017-06-16 Thread Nourah mmm
Hi,

I try to run KLEE on cutcp benchmark from (Parboil Benchmarks
). The benchmark
consists from the following program: main.c  parboil.c readatom.c cutcpu.c
excl.c output.c

First I compile it with the following command:
myclang -I /home/klee/klee_src/include -emit-llvm -c -g main.c  parboil.c
readatom.c cutcpu.c excl.c output.c

Then, I run KLEE with this command:
myklee --posix-runtime --libc=uclibc  --link-llvm-lib=parboil.bc
--link-llvm-lib=cutcpu.bc --link-llvm-lib=excl.bc --link-llvm-lib=output.bc
--link-llvm-lib=readatom.bc ./main.bc -i
/home/naloboud/parboil/datasets/cutcp/small/input/watbox.sl40.pqr

However I get this error:
KLEE: NOTE: Using model:
/home//klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: Linking in library: parboil.bc.

KLEE: Linking in library: cutcpu.bc.

KLEE: Linking in library: excl.bc.

KLEE: Linking in library: output.bc.

KLEE: Linking in library: readatom.bc.

KLEE: output directory is "/home//klee/examples/cutcap/./klee-out-10"
Using STP solver backend
KLEE: WARNING: undefined reference to function: __isoc99_sscanf
KLEE: WARNING: undefined reference to function: ceilf
KLEE: WARNING: undefined reference to function: fabs
KLEE: WARNING: undefined reference to function: feof
KLEE: WARNING: undefined reference to function: fgets
KLEE: WARNING: undefined reference to function: floorf
KLEE: WARNING: undefined reference to function: fmaxf
KLEE: WARNING: undefined reference to function: fminf
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING: undefined reference to function: sprintf
KLEE: WARNING: undefined reference to function: sqrtf
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 53351024)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: gettimeofday(53752832, 0)
KLEE: WARNING ONCE: calling external: fgets(53760304, 96, 53770848)
KLEE: ERROR: /home//klee/examples/cutcap/readatom.c:44: failed external
call: fgets
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 12343
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1


Could you please help me with that?
Thanks
Nourah
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev