Presumably, you are doing something other than just incrementing i in the loop, though.

Most of the time with Frama-C, all you have to provide is function pre- and post-conditions and loop invariants.