--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] operator %



Is it really a bug in the lithium version?
I put your code in a file misc.c and run
frama-c -jessie-analysis -jessie-int-model exact -jessie-gui misc.c
I am using lithium on Mac OS X and obtain the following results (that  
look fine to me).

Regards Jens




Am 06.04.2009 um 13:03 schrieb Omar Chebaro:

> thanks to pascal we know that this is a bug that existed in the  
> lithium
> version (the one I use), and is now fixed in the current development
> version
>
> On Mon, 2009-04-06 at 12:23 +0200, Claude March? wrote:
>> And regarding jessie, there is also a unproved VC. So what is the  
>> problem?
>>
>> - Claude
>>
>> Benjamin Monate wrote:
>>> Hi,
>>>
>>> frama-c -val gives :
>>>
>>> t.c:5: Warning: division by zero: assert (n <> 0);
>>>
>>> What else do you expect ?
>>>
>>> Cheers,
>> _______________________________________________
>> 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
>
>
> _______________________________________________
> 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


-- 

Dr.-Ing. Jens Gerlach
Eingebettete Systeme - EST
Tel.: +49 (0)30 6392 1841
Fax.: +49 (0)30 6392 1805
E-Mail: jens.gerlach at first.fraunhofer.de

Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST
Kekul?stra?e 7
12489 Berlin
Germany
http://www.first.fraunhofer.de




-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090406/ded28b48/attachment-0001.htm 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: lithium.tiff
Type: image/tiff
Size: 52300 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090406/ded28b48/attachment-0001.tiff