Frama-C has a wp plugin that generates assertions about overflow and underflow, which is one of the best tools it has. It's not spectacular about telling you where the problem is, and wasn't great with floats, though.