--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] With Why version 2.23, Jessie binary_search example fails. Why?



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