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: anne.pacalet at free.fr (Anne Pacalet)
  • Date: Thu, 25 Apr 2013 13:56:55 +0200
  • In-reply-to: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
  • References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
Hello,

First of all, many thanks for this new version of Frama-C.
The compilation of my plug-ins went smoothly, and the modification
where mainly about the Printer and the new 'category' log feature.

Nevertheless, some remarks about (little) things that are not working :


- 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.


- #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 :-(


- 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.

- 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 ?


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