In my case, the klee only generates one path and one test. How many
paths and tests that the test generator should generate for my program?
( I think it should be 32).
Hi Thanh, since you're not marking anything as symbolic, there is only
one path through the program, as in a normal
Hi Daniel,
Thank you for your answer.
However, when I run klee with uclibc flag, Klee still dumps error message
like this
klee --libc=uclibc input.o
klee: error: Cannot find linker input '/lib/libc.a'
klee: ModuleUtil.cpp:42: llvm::Module* klee::linkWithLibrary(llvm::Module*,
const
Hi Thanh,
KLEE doesn't support symbolic floating point currently, mostly just
because STP doesn't support it, although it would probably still be an
option because the performance is likely to be very poor.
What KLEE currently does is concretize the value (pick some feasible
value, and
Hi,
I am using Klee to generate tests for floating point programs. However, even
with some simple program, Klee can not generate a full test cases for the
program. As with following simple code:
1. #include stdio.h
2. #include float.h
3. #define NAN 0.0/0.0
4. #define INF 1.0/0.0
