--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on December 2009 ---
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