[LLVMdev] Current work on type-safety proving?

[Jules]

I was just wondering what existing work has been done on proving
programs type-safe using the LLVM framework?  I've read the paper on
memory-safety for embedded systems, but that's not quite what I'm
looking for, as my application (which involves running untrusted code
within a trusted context) might fail if a pointer to one object became a
pointer to another of the same type.

Looking at the documentation, it seems a trivial check for type-safety
would be simply to ensure that the program didn't use any 'cast'
instructions, only used the memory allocation facilities of a trusted
garbage collector, and didn't contain any zero-length arrays (as these
might be used for unsafe pointer arithmetic).  However I guess that in
the real world, these constraints would be almost impossible to program
to (e.g., my simple C++ test programs suggest that it's impossible to
write any non-trivial C++ program that doesn't generate a 'cast'), so
there must be circumstances that allow such constructs.

Has any work been done on this?  If not, what pointers would you give
for places to start?

Thanks,

Jules