--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2009 ---
[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                    |