[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