Discussion:
make klee support intrinsic function lvm.sadd.with.overflow.i32
(too old to reply)
Dingbao Xie
2014-10-16 23:23:15 UTC
Permalink
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
Daniel Liew
2014-10-17 09:49:23 UTC
Permalink
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
2014-10-17 09:50:11 UTC
Permalink
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
Loading...