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?

Hello (and Happy new year to everybody ;-),

Le sam. 02 janv. 2010 22:32:02 CET,
"David A. Wheeler" <dwheeler at dwheeler.com> a ?crit :

> * When I downloaded & installed the new Why version 2.23, the same example STOPPED working.  With Why version 2.23, there were 4 more safety VCs named "variant decreases".  Two of the 4 new ones are easily proved by alt-ergo.  But two of the generated VCs try to prove "0<0", which obviously CANNOT be proven.
> 

I guess that this new behavior is caused by this item in the Changelog
of Why (why 2.22)

o [Jessie][Frama-C] bug fix: 0103. Loops without variant are given a
      default unprovable variant. 

In other words, while previous versions would generate VCs related to
termination only in presence of an explicit loop variant (partial
correctness), in why 2.23 you always have those VCs, with a default,
non-decreasing variant (the constant 0 as a matter of fact).
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. 

Hope this helps,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98