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] Semantics of Jessie icons?
- Subject: [Frama-c-discuss] Semantics of Jessie icons?
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Fri, 27 Mar 2009 12:25:04 +0100
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com> <firstname.lastname@example.org> <email@example.com>
valid (green dot) : the VC is a true formula invalid (red dot) : the VC is not a true formula unknown (question mark) : it is not known if the formula is true or not timeout (scissor) : the prover did not answer before the timeout (10 s by default) failure (tools) : the prover answer was not recognized (hard disk) : this VC is already known valid in GWhy cache * the shape of the icons varies among users, becasue these are builtin GTK icons, which depend on the current gtk theme * in principle, invalid should be identified with unknown, because provers are incomplete can very rarely say that a formula is definitely not true. historically, Simplify answers is either "valid" or "invalid", where "invalid" indeed means "unknown". The GWhy maps those invalid to the question mark but the textual output might still classified them as invalid. * the cache feature is not really used: the VCs in cache are still rerun in provers. * failure might have many causes: fail to run prover's process, syntax error in the output file, etc. In case of failure, one can inspect the problem by activating debug (menu Proof/Debug mode) and look at the debugging output in the console. - Claude PS: I support the idea of setting-up a wiki so that this kind of info could be more persistant. David MENTRE wrote: > On Fri, Mar 27, 2009 at 11:44, David MENTRE <dmentre at linux-france.org> wrote: >> On Thu, Mar 19, 2009 at 09:55, David MENTRE <dmentre at linux-france.org> wrote: >>> What is the exact semantics of Jessie GUI icons? > [...] >> So I think we have: >> * valid : green dot >> * invalid : ?? >> * unknown : question mark >> * timeout : scissors >> * failure : ?? >> >> What is the difference between "failure" and "invalid"? >> >> What is the difference between "unknown" and "timeout"? > > And what does mean the "hard disk" icon? > > Yours, > d. > > _______________________________________________ > 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 -- 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 |