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] new GWhy - statistics


Le 09/10/2013 20:17, Nanci Naomi a ?crit :
> Hello,
> 
> We were used to the old interface of Frama-c/Jessie/Why.
> 
> Now, we are using the Why3 Verification Platform 0.81, Fluorine-20130601
> and we have some doubts:
> 
> 1 - how to find the statistics? In the old version, the provers were
> shown in columns and in the right it was shown how many VCS were
> generated and proved. 

if your file is f.c, then the why3 session is stored in

f.jessie/f/why3session.xml

You have several ways to obtain statistics :

1) some statistics in text format

  why3session info --stats f.jessie/f

2) detailed info in HTML format:

  why3session html f.jessie/f

then open f.jessie/f/f.html in your favorite web browser

3) detailed info in LaTeX

  why3session latex <options> f.jessie/f

See the Why3 manual, section on why3session, for more details.

If you are interested in a particular kind of statistics that is not
provided, please ask, Why3 developers may be willing to provide it.

- Claude

> 2 - when a VC is selected, in the bottom right window is shown the code
> with highlighted lines in yellow and green. What does the colors mean?
> In the old version, the related code lines were shown only in yellow.

In yellow (or orange ?) is the goal, in green the hypotheses

> 3 - is there a manual that explain the new interface?

The Why3 manual, http://why3.lri.fr

> Regards
> Nanci Naomi

All the best,

- Claude


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |