--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2010 ---
Virgile Prevosto <virgile.prevosto at cea.fr>: > If you add a loop variant in the loop annotation, i.e. > loop variant u - l; > then all proof obligations (in the exact integer model) are proved. Thanks! I'd tried that out before, but it had subtly failed, and I ended up thinking that loop variants weren't supported. It turned out that my problem was that I did this: //@ loop invariant 0 <= l && u <= n-1; //@ loop variant u-l; But two adjacent "//@" lines do NOT work. What's more, this gave an incredibly misleading error message in a far later line, and that's why I thought loop variants were unsupported. Once I changed it to this, it worked: /*@ loop invariant 0 <= l && u <= n-1; loop variant u-l; */ Thanks again. --- David A. Wheeler