Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with bitwise xor

OK, I see now your problem. Thanks for the report.

- Claude

Hollas Boris (CR/AEY1) wrote:
>> Sorry for the dumb answer:  with which values of x and y do not you
>> think there is an overflow ?
>>     
>
>   
>> I don't even understand what arithmetic overflow may mean for xor.
>>     
>
> Jesse generates VC for arithmetic overflow and can't prove them. You are right that with bitwise operations, no overflow can occur. Still Jessie tries to verify sth and fails. Hence, I don't get green bullets for this code.
>
> I filed bug report http://bts.frama-c.com/view.php?id=348 on this.
>
> -Boris
>
> _______________________________________________
> 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
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |