[klee-dev] klee and overshift error

[Andrew Santosa]

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_2006 at 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 at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed