I've used CIL (if only for school projects), and I can vouch for it being a joy to use, at least if you like OCaml. Also, their page on wacky C edge cases ("Who says C is simple?", link to frame contents: http://www.cs.berkeley.edu/~necula/cil/cil016.html") is great.
