Since Shap has frequently bemoaned the use of an unsafe language for LLVM, there is some promising work in this direction:
http://lambda-the-ultimate.org/node/4440 The relevant point: To demonstrate Vellvm's practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm's tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the non-verified, ad-hoc original. Sandro _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
