[klee-dev] KLEE finishes fast

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>