--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on October 2013 ---
[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                    |