Frama-C does not say much, when do don't tell it what it should do. It needs to reason over symbolic facts, C code is not enough. It's not just another simple static code checker.

You can look at the Frama-C blog what it does with a major openssl competitor, polarssl. http://blog.frama-c.com/