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?

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                    |