[LLVMdev] New automated decision procedure for path-sensitive analysis

[Zhongxing Xu]

>
> Spear takes a different approach - it is bit-precise, handles all
> operators, but
> currently doesn't handle arrays directly. However, the other mentioned
> thm provers
> handle arrays by encoding them as UIFs + several axioms. As UIFs can be
> encoded
> to SAT, I think that the theory of arrays could be as well. So, with a
> bit of effort,
> you should be able to use Spear for reasoning about arrays.
>
> Thank you. I will try it.
But what I really mean is that array simulation is not an adequate solution
to pointer problems. :-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20070409/85530835/attachment.html>