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

[Domagoj Babic]

Hi,

On 4/8/07, Zhongxing Xu <xuzhongxing at gmail.com> wrote:
> Thank you. I will try it.

Np.

> But what I really mean is that array simulation is not an adequate solution
> to pointer problems. :-)

If you are only interested in a single abstract memory location per allocation
site, that can be handled efficiently. For structured graphs, symbolic
execution can be done very efficiently. I'd give you a reference, but
it's in submission
:-) . Once computed, definitions of abstract memory locations are bit-precise,
and you can pass such queries to Spear.

Proving properties for some more complex data structures than arrays can be
done, but I'm not an expert in that field, so can't give you good
references. The
best I can tell you is to google for shape analysis and separation logic.

Anyways, this is off-topic. If you have further questions/comments on
handling arrays/pointers/memory, please email me directly.

Domagoj Babic