--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unproven VC with newer why version



> 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.