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