--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Frama-C version: Fluorine



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