--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on December 2014 ---
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