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

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



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>