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?
- Subject: [Frama-c-discuss] Res: Feature or bug?
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Thu, 12 Nov 2009 10:01:51 +0100
- In-reply-to: <0C9ECAC2-CC68-4159-A272-7098A7B05E34@first.fraunhofer.de>
- References: <42152DCA-6856-46A4-A072-F564021DF6DD@first.fraunhofer.de> <4AF32BE9.2070904@inria.fr> <416973.53148.qm@web32901.mail.mud.yahoo.com> <4AF8495C.5000400@inria.fr> <0C9ECAC2-CC68-4159-A272-7098A7B05E34@first.fraunhofer.de>
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 |
- References:
- [Frama-c-discuss] Feature or bug?
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] Feature or bug?
- From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
- [Frama-c-discuss] Res: Feature or bug?
- From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
- [Frama-c-discuss] Res: Feature or bug?
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Res: Feature or bug?
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] Feature or bug?
- Prev by Date: [Frama-c-discuss] Frama-C vs Ada/SPARK
- Next by Date: [Frama-c-discuss] Newbie question
- Previous by thread: [Frama-c-discuss] Res: Feature or bug?
- Next by thread: [Frama-c-discuss] ask for slicing spec
- Index(es):