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