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@xxxxxxxxxxxx> 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. _______________________________________________ package-review mailing list package-review@xxxxxxxxxxxxxxxxxxxxxxx https://admin.fedoraproject.org/mailman/listinfo/package-review