--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problems with recognition of the variant



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>