Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] With Why version 2.23, Jessie binary_search example fails. Why?
  • From: dwheeler at dwheeler.com (David A. Wheeler)
  • Date: Mon, 04 Jan 2010 11:02:38 -0500 (EST)
  • In-reply-to: <20100104111750.1b613521@is010235>
  • References: <E1NRHCE-0007aW-Gi@fenris.runbox.com> <20100104111750.1b613521@is010235>
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