Re:Frama-C: Modular Analysis of C Programs
by im3w1l on Tuesday October 06, 2020 @12:01PM
(#24699161)
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.
[ Parent
| on HN ]
Re:Frama-C: Modular Analysis of C Programs
by Jtsummers on Tuesday October 06, 2020 @12:14PM
(#24699334)
My 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.
Re:Frama-C: Modular Analysis of C Programs
by mcguire on Tuesday October 06, 2020 @12:26PM
(#24699533)
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.