[klee-dev] make klee support intrinsic function lvm.sadd.with.overflow.i32

Daniel Liew daniel.liew at imperial.ac.uk
Fri Oct 17 10:49:23 BST 2014


Hi,

On 17 October 2014 00:23, Dingbao Xie <xiedingbao at gmail.com> wrote:
> Dear list,
> I found that klee dose not support the LLVM arithmetic with overflow
> intrinsics
> like llvm.sadd.with.overflow.i32. I know that someone else has asked the
> similar
> question. I just want to know is it possible to make klee support it?
> Thanks in advance

This is possible. I think the correct way to do this would be to add
support for it in the IntrinsicCleaner pass [1]. You can see that
Intrinsic::uadd_with_overflow support is handled so I think you would
need to add support for the signed version.



[1] https://github.com/klee/klee/blob/master/lib/Module/IntrinsicCleaner.cpp

Thanks,
Dan.




More information about the klee-dev mailing list