[LLVMdev] secure virtual architecture / safecode

[John Regehr]

On Wed, 25 Mar 2009, Vikram S. Adve wrote:

> We do have a static array bounds checking algorithm based on the Omega
> integer programming library, but it is not hugely effective.  I think
> this can be strengthened a *lot*.

I should add that I would be interested in helping with hooking a good 
decision procedure into LLVM.  This will be useful far beyond array bounds 
check elimination.

What is the current thinking?  SMT solver?

John