--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on December 2009 ---
> Would it be useful to add automatically a clause "variant N-i;" for > loops having the simple syntactic structure "for (i = ... ; i < N ; > i++)"? This way proof obligations for such loops (which are quite > common) would be automatically discharged. > Regards, > david In C, the loop variable can be modified in the body. Hence, The loop variant you propose may not hold. If a variant was added automatically, it wouldn't be possible to verify these loops. The same is true for loop invariants. A solution is to use abstract interpretation to infer simple loop invariants and variants automatically.