[klee-dev] klee and overshift error

[Dan Liew]

On 22 July 2017 at 16:49, Andrew Santosa <asantosa1999 at 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.