[klee-dev] Klee badvector access error

[Frank Busse]

Hi Mohit,


On Thu, 3 Jun 2021 11:02:11 +0530 (IST)
kmohit <kmohit at cdac.in> wrote:

>  I am using  KLEE-2.1. Can anyone provide an example with source code
> where KLEE is able to detect "badvector access" error ?

I'm not sure if I can come up with a C-only example. But you can
compile:

--
#include <immintrin.h>

int main(void) {
	__m128 A, B;
	_mm_add_ss(A, B);
}
--

with -msse, disassemble the bc file (llvm-dis), manipulate the
insertelement instruction e.g. to (0 -> 42):

%13 = insertelement <4 x float> %12, float %11, i32 42

re-assemble (llvm-as) and run KLEE. It'll find the out of bound access
(bad_vector_access.err).


Kind regards,

Frank