Hi Mohit,
On Thu, 3 Jun 2021 11:02:11 +0530 (IST) kmohit <[email protected]> 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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
