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] possible bug in bitwise operators and jessie

Damien Karkinsky wrote:
> Hello,
>
> I can't get any of the provers to prove the following:
>
> void function(){
>     /*@ assert (3&1) == 1*/
> }
>
>   
I guess you mean you can't prove it with the Jessie plugin ?
> Can anyone shed some light or is this a bug?
>
>   
A *bug* in the jessie plugin can be either

- an unexpected fatal error raised in the tool chain which generates the 
VCs (typically "assert failure" and such...)
- a wrong property that would be proved correct

So in your case, it is not a bug, just an *incompleteness*.

You're right, the Jessie plugin poorly supports bitwise operations.
Some improvements have been done in the development version recently,
so you can hopefully expect a better support in the next release of Why.

- Claude

-- 
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                    |