[Frama-c-discuss] possible bug in bitwise operators and jessie

Claude Marche Claude.Marche at inria.fr
Mon Feb 15 09:30:12 CET 2010


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                    |




 





More information about the Frama-c-discuss mailing list