[Bug 564520] Review Request: frama-c - Framework for source code analysis of C software

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=564520

--- Comment #8 from David A. Wheeler <dwheeler at dwheeler.com> 2010-02-15 21:00:48 EST ---
Note: Fedora packages Why version 2.23, not Why version 2.21.
That's not a problem, in fact, that's a GOOD thing
(Why version 2.23 has many more capabilities).
However, it means that the Frama-C documentation for
Jessie does NOT work as-is, because they changed a default setting in
Why's Jessie.

So, what's changed?
As of Why version 2.22, Jessie now requires proof of
termination by default.  This is a good change, because the previous
semantics were tripping people up.  The newer versions of Why also
have FAR better support for termination proofs (since they made it the
default, they suddenly had to support it better :-) ).
However, since it no longer works as-is with the included docs, there
should be SOMETHING in the package that documents this change.

So I recommend including a file with the following content, or something
like it, as a %doc.   Call it "frama-c-1.4.why-changes.txt" or
something like it:

============================================================
Note that when Frama-C is used with Why version 2.22 or greater, there
is an important change in the semantics of Jessie.

In Why version 2.21's Jessie component, by default you did NOT need
to prove termination.  This resulted in some surprises and problems for users.
Thus, starting in Why version 2.22, Jessie requires proof of
termination by default.

As a result, many of the examples in the Frama-C Beryllium documentation
for Jessie do not work as-is, because they
don't include termination information.  For more information, see:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001736.html

For example, the Jessie tutorial section 2.2 needs to have a "loop variant"
added.  What's more, this MUST be added using
the /*@...*/ form NOT the //@ forms (you can't have adjacent //@ forms).
Here is what the updated example in section 2.2 looks like:

/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */

//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1, p = -1;
  /*@ loop invariant 0 <= l && u <= n-1;
    @ loop variant u-l; */
  while (l <= u ) {
    int m = l + (u - l) / 2; // NOTE this is changed for bounded calculation
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else {
      p = m; break;
    }
  }
  return p;
}

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.