Curious if the folks at OpenBSD have ever thought about giving CompCert-C a shake. I realize it's no gcc or llvm, but OpenBSD is no run of the mill *nix, either.

http://compcert.inria.fr/compcert-C.html

EDIT: See also https://github.com/AbsInt/CompCert