make klee support intrinsic function lvm.sadd.with.overflow.i32

[Dingbao Xie]

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

[Daniel Liew]

Hi,

Post by Dingbao Xie
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.

[Mark R. Tuttle]

Luca Dariz showed us a solution for unsigned. I want to finish that off for
signed. I am new to the llvm IR and am slowed by that learning curve. Mark

Post by Dingbao Xie
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
--
Dingbao Xie
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev