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] Res: Feature or bug?



Jens Gerlach wrote:
> Am 09.11.2009 um 17:54 schrieb Claude Marche:
>
>   
>> Could you explain why this behavior really annoys you ?
>>     
>
> I wouldn't use the word "annoy", but looking at my original example (see below)
> the different answers from the provers might appear at first sight as inconsistent.
>
>   
For me, on this example, all answers of provers are consistent, so I 
don't understand.

> It also reminds me of the "green follows orange" feature of Polyspace (http://www.mathworks.se/access/helpdesk/help/toolbox/polyspace/c_ug/brj0wna-1.html)
> which in my experience bothers some users.
>
>   
Nice to known about. Did polyspace developers changed something about that ?

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