[LLVMdev] New automated decision procedure for path-sensitive analysis
xuzhongxing at gmail.com
Sun Apr 8 22:30:45 PDT 2007
> 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
> 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...
More information about the llvm-dev