--- layout: fc_discuss_archives title: Message 15 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



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

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com