--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2014 ---
You can also add a lemma or axiom asserting the decreasing of the shift, or the equivalence of shifting and dividing for the desired constants. L. Le 12 d?c. 2014 ? 09:13, BAUDIN Patrick <Patrick.Baudin at cea.fr> a ?crit : > Your code was : > void testVariant(unsigned long n) { > unsigned long i= n; > /*@loop variant i;*/ > while (i >= 2UL) { > i >>= 2UL; > } > } > Replacing the shift by integer division is a good idea since it could help to get automatic proof (the use of the shift will require a coq proof). > That will help you in guessing the missing loop invariants. > They are needed for the proof of your loop variant. > Also, perhaps that "i/2" is a better variant. > > Le 12/12/2014 08:22, Roberto Bagnara a ?crit : >> On 20/11/2014 18:03, ALESSIO BORTOLOTTI wrote: >>> While I was trying to prove a while loop containing shifts, I ran into a problem: the program couldn't recognize the variable on which I have done the shift as a variant. >> I stumbled upon the same issue. Apparently the latest version >> of Frama-C is not able to prove that a nonzero unsigned quantity >> shifted to the right by a nonzero number of positions results >> in a strict decrease. Replacing shift by integer division does >> not help. Can someone on this list explain what is going on? >> Is there a workaround for this problem? >> Kind regards, >> >> Roberto >> > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141212/b714a0b8/attachment-0001.html>