Hi,
Without including the program, it's not clear whether KLEE should have
run for longer. One relevant thing one can tell from the log is that
KLEE concretized a symbolic object size.
Best,
Cristian
On 24/03/2020 09:45, XIE Xuan wrote:
Dear KLEE,
I am running KLEE on a fuzzing dirver. But KLEE finish in a few seconds.
And it generates warning shown below. I don’t know whether it is because
of the missing of math function (but those are floating math function,
which is not supported by KLEE anyway). Do you have any idea of how to
debug it? I am happy to provide more information if needed!
```
KLEE: NOTE: Using POSIX model:
/root/trial/klee/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using klee-uclibc :
/root/trial/klee/build/Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/root/tmp/ "
KLEE: Using STP solver backend
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: WARNING: undefined reference to function: __fpclassifyf
KLEE: WARNING: undefined reference to function: __isinf
KLEE: WARNING: undefined reference to function: __isnanf
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: exp
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: floorf
KLEE: WARNING: undefined reference to function: llvm.fabs.f32
KLEE: WARNING: undefined reference to function: llvm.fabs.f64
KLEE: WARNING: undefined reference to function: log
KLEE: WARNING: undefined reference to function: log10
KLEE: WARNING: undefined reference to function: pow
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sqrt
KLEE: WARNING: undefined reference to function: sqrtf
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505,
93958238439968) at /root/trial/klee/runtime/POSIX/fd.c:990 10
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not
modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: gettimeofday(93958238379168, 0) at
/root/trial/klee/runtime/POSIX/stubs.c:174 7
KLEE: ERROR: cmserr.c:97: 0.486355: concretized symbolic size
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 90013
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3
```
Best Regards,
Xuan XIE
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
