--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2010 ---
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