3 ms·
This sounds like an invariant even an optimizing compiler could find, because it's such a common construct. Well... I guess they have an easier job because they
by im3w1l 6y ago
This sounds like an invariant even an optimizing compiler could find, because it's such a common construct. Well... I guess they have an easier job because they can "assume away" signed overflow.
- Jtsummers 6y agoMy point was that that may not be the actual invariant. By making your invariants explicit these tools have a better chance of finding real errors since you compare the code against a specification. Deriving a specification just means your code works according to itself.
- mcguire 6y agoPresumably, 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.