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

[Frama-c-discuss] RE : RE : RE : plugin incompatible with Fluorine



Hello,

Don't know what exactly happens here. When Frama-C cannot load a found plug-in, it displays a warning like this:
$ frama-c
[kernel] warning: cannot load 1 plug-in (incompatible with Fluorine-20130501+dev).
                  E_ACSL

If you don't have such a warning, either the plug-in is not found (so it is not installed in the proper directory), or it is found but it does nothing. You can check that by running `frama-c -plugin-name-help` like this (here you get a user error because the plug-in is not found):
$ frama-c -e-acsl-help
[kernel] warning: cannot load 1 plug-ins (incompatible with Fluorine-20130501+dev).
                  E_ACSL
[kernel] user error: option `-e-acsl-h' is unknown.
                     use `frama-c -help' for more information.
[kernel] Frama-C aborted: invalid user input.

Hope this helps,
Julien

________________________________
De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Maria Christofi [maria.christofis at gmail.com]
Date d'envoi : vendredi 23 ao?t 2013 12:27
? : Frama-C public discussion
Objet : Re: [Frama-c-discuss] RE : RE : plugin incompatible with Fluorine

Hello,
Thanks for the script.

That's what I did (with make clean etc). I checked in the frama-c/plugins and the .cmo and .cmxs of the plugin are there, but I still cannot use it...

Maria

2013/8/23 SIGNOLES Julien <julien.signoles at cea.fr<mailto:julien.signoles at cea.fr>>
Hello,

Oh yes, nitrogen2oxygen seems to be missing in the Oxygen release. Actually it fixes only few issues, so it is probably useless in your code. I attach it to this mail anyway. You can check if you have to apply it by reading it: the script's core is a sed command replacing OCaml terms by some others. If you don't use any of these terms, the script is useless in your case.

When changing of Frama-C version (or OCaml version), you have to run "make clean" before: "make clean && make && make install". If all is ok, your plug-in is installed by default in `frama-c -print-plugin-path` (.cm[io] and .cmxs files in the standard case). You can also check that you're using the right frama-c version by running "frama-c -version".

Hope this helps,
Julien

________________________________
De : frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr>] de la part de Maria Christofi [maria.christofis at gmail.com<mailto:maria.christofis at gmail.com>]
Date d'envoi : vendredi 23 ao?t 2013 10:50
? : Frama-C public discussion
Objet : Re: [Frama-c-discuss] RE : plugin incompatible with Fluorine

Hello Julien,

Thank you for your answer!

As there were no bin/nitrogen2oxygen.sh script with the oxygen release I thought that it was fully compatible (wrong... ), I ve run directly the oxygen2fluorine.sh.. Where could I fid the nitrogen2oxygen script?

But what I find more weird is that my plugin compile correctly with the "make && make install" with no errors. but it is still no installed.. I should have some errors during the compilation, isn't it?

Maria


2013/8/23 SIGNOLES Julien <julien.signoles at cea.fr<mailto:julien.signoles at cea.fr>>
Hello,

Indeed we usually break some APIs at each major release, because it is hard to make Frama-C evolve without changing them. But we also provide scripts to convert plug-ins to the new version. Here you directly upgrade from nitrogen to fluorine by skipping oxygen. So you have to apply first the script bin/nitrogen2oxygen.sh, and next the script bin/oxygen2fluorine.sh provided in the corresponding source tarballs (don't know whether packagers install these scripts or not). But the chemical process to convert nitrogen to fluorine is a bit complex ;-) and it may remain some unconverted part in your code depending on what it uses. In such a case, you can post on this list what remains to change and we will help you.

Hope this helps,
Julien Signoles

________________________________
De : frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr>] de la part de Maria Christofi [maria.christofis at gmail.com<mailto:maria.christofis at gmail.com>]
Date d'envoi : jeudi 22 ao?t 2013 19:22
? : Frama-C public discussion
Objet : [Frama-c-discuss] plugin incompatible with Fluorine

Hello again (it s still me....)!

After succesfully installing Frama-C Fluorine, I wanted to regain my old habits and tried to reinstall a plugin that I had developped and worked with Frama-C Nitrogen.
But I didn't manage it with an error of incompatibility with Fluorine.
Before spend any time on it, did anyone have the same kind of error and has an idea of where should I look for a solution?
(apologies for not giving more precisions...)

Thanks in advance!

--
Maria Christofi

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



--
Maria Christofi

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



--
Maria Christofi
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130824/e27d5240/attachment.html>