--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on December 2014 ---
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 > -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141212/bb5aa974/attachment.html>