--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on February 2010 ---
[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                    |