I believe the -fsanitize=undefined option turns on all checks done by
clang's undefined behavior sanitizer except for unsigned-integer-overflow.
So -fsanitize=undefined implies -fsanitize=signed-integer-overflow which
will cause clang to generate the signed llvm.*.with.overflow instrinsics
which klee does not yet support. I believe you will get the same result if
you replace -fsanitize=undefined with -fsanitize=signed-integer-overflow
A handful of people on this list are interested in these intrinsics, and
from among them some implementation of these instrinsics is likely to
Post by Dingbao Xie
I got an LLVM error when using klee to analyze a program generated by
I tried to debug it by myself and finally found that the error is produced
PassManager.run (klee/lib/Module/KModule.cpp, function prepare, pm3.run).
LLVM ERROR: Code generator does not support intrinsic function
Attachment is the test program that I used.
Does anyone know why LLVM produced such error and how can I get around it.
BTW I built klee with LLVM-3.4.
Thanks in advance.
klee-dev mailing list