--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on March 2009 ---
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 |