--- layout: fc_discuss_archives title: Message 78 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



Hello,

2009/12/8 Claude Marche <Claude.Marche at inria.fr>:
> In a nearer future, there could a new pragma to control the generation
> of such VCs.
>
> Anyway: any suggestion welcome !

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