On 22 July 2017 at 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 being > shifted.
Slight correction. KLEE will report an error if the shift width is greater than **or equal to** the bitwidth being shifted because at the LLVM IR level (and at the level of C) this is undefined behaviour. > > 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 If you really don't care about the undefined behaviour you can remove the check by passing `-check-overshift=0` to klee. You should be careful though. Having undefined behaviour in your program may cause you problems. HTH, Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
