Thank you Andrew and Dan for your response. I have tried to measure the
coverage with the generated test cases and it is very low. The test cases are
generated based on choosing N and X variables ( main inputs of the libquntukm
program) to be symbolic inside the code with using klee_make_symbolic. I also
tried KLEE with Hmmer program in SPEC benchmark to generate more test cases
with using klee_make_symbolic but I still couldn't achieve a high coverage.
Do you have any suggestions to generate more test case and achieving high
coverage using Klee with SPEC benchmarks?Thank you.
On Saturday, 22 July 2017, 16:49, Andrew Santosa <asantosa1...@gmail.com>
wrote:
Hi BNM,
KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM.It
is reported when KLEE determines that the shift amount is greater than the
bitwidth of the data beingshifted. I happen to have a copy of SPEC CPU 2006. At
Line 108 of classic.c there is a loop whose entrycondition includes a left
shift. It is possible that nothing gets reported when the program is run
natively.
Best,Andrew
On Sun Jul 16 2017 00:38:50 GMT+0800 (SGT), BNM <boooth_2...@yahoo.com> wrote:
Hello,
I have tried to run Klee with libQuantum in SPEC benchmarks. The duration of
running Klee with this benchmark lasted more than 24 hours and all the test
cases contained overshift error.
KLEE: ERROR: /klee/libqu/classic.c:108: overshift error
I would like to know what is the cause of this error? Is it related to the
choice of the symbolic variable? Without using KLEE the benchmark works well.
Thank you,
_______________________________________________
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
