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 Frama-C version: Fluorine

  • Subject: [Frama-c-discuss] New Frama-C version: Fluorine
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Mon, 06 May 2013 13:42:40 +0200
  • In-reply-to: <51791A07.40706@free.fr>
  • References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com> <51791A07.40706@free.fr>
Hello Anne,

Thanks for your quick feedback.

On 04/25/2013 01:56 PM, Anne Pacalet wrote:
> - thanks to have added Datatype.Triple, but Type.pp_ml_name seems to be
> incorrect. Bts #1127 is fixed for Datatype.pair, but Triple leads to
> Datatype.Triple.instantiate which is not recognized later on :
> Error: Unbound value Datatype.Triple.instantiate
> $ sed -i "s/Datatype.Triple.instantiate/Datatype.triple/g" api.ml
> fixes the problem.

True. Should now be fixed.

> - #1287 is said to be fixed, but in fact, frama-c.toplevel is not working
> anymore :-( It just returns and does nothing...
> Moreover, it doesn't understand the usual toplevel options like -I
> or -init. It seems to me that this is not an ocaml toplevel...
> This problem is the more serious one since I think that I have
> no idea of how to go arround :-(

True. When I tested it few months ago, it worked fine as fas as I 
remember. Meanwhile, I upgraded my OCaml compiler to 4.*. I just 
discover that there are non trivial issues between the Frama-C libraries 
and the OCaml 4.* standard libraries included in the toplevel. 
Unfortunatly I see no simple solution and I'm affraid that an usable 
Frama-C toplevel will only be available through a commercial offer 
(http://frama-c.com/support.html).

> - bts #1278 about the internal doc directory is said to be fixed,
> but it is not. When I do :
> $ make install-doc-code
> It still install my documentation in /usr/local/share/frama-c/doc/XXX
> while the doc of the other plug-ins are in
> /usr/local/share/frama-c/doc/code/code/
> So the link to ../index.html (from code/intro_plugin_default.txt)
> are broken.

What have been fixed is the installation of the plug-in doc through the 
Frama-C Makefile. Installation of the doc through the plug-in's Makefile 
is fixed now.

> - in the INSTALL file, the "API DOCUMENTATION" section refers to
> frama-c-api.tar.gz
> which is supposed to be created by "make doc". I don't find it,
> and I was wondering if it is the same thing that what is installed in
> /usr/local/share/frama-c/doc/code ?

Actually, the right target of the Makefile to create the tarball is 
"doc-distrib". INSTALL file is fixed.

> That's all for now, but I decided now to try the new ocaml version,
> so maybe some more problem to come... ;-)

Feel free to report additional problem if any. BTW do not hesitate to 
(re)open task on the BTS in case of issues.

--
Julien