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 itself.
See http://clang.llvm.org/docs/UsersManual.html#id30. A handful of people on this list are interested in these intrinsics, and from among them some implementation of these instrinsics is likely to emerge soon. Mark On Fri, Oct 17, 2014 at 9:02 PM, Dingbao Xie <[email protected]> wrote: > Hi all, > I got an LLVM error when using klee to analyze a program generated by > clang-3.4. > I tried to debug it by myself and finally found that the error is produced > when calling > PassManager.run (klee/lib/Module/KModule.cpp, function prepare, pm3.run). > > The detailed error information is: > LLVM ERROR: Code generator does not support intrinsic function > 'llvm.sadd.with.overflow.i32'! > > 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. > > > > -- > Dingbao Xie > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
