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] [Why3-club] Using Why3 api in frama-c plugin


  • Subject: [Frama-c-discuss] [Why3-club] Using Why3 api in frama-c plugin
  • From: 7jpinheiro at gmail.com (José Pinheiro)
  • Date: Fri, 5 Sep 2014 21:41:39 +0100
  • In-reply-to: <5409FF58.6010202@inria.fr>
  • References: <CAM1QBJPSxOFR_XFUxaUmoyso-_kZDP6ZBLeN-ytmTaVEEuBiMA@mail.gmail.com> <5408B32C.70704@inria.fr> <CAM1QBJPA65qKmKLMP3=qdRrX=5ncdRiWu9fYPgHabKrADPpHig@mail.gmail.com> <5409FF58.6010202@inria.fr>

Yes, i checked they are correctly installed and i also tested using the
$(shell frama-c -print-lib-path) and  $(shell frama-c
-print-share-path) accordingly.

I was able to fix the error, by opening on the source code of the plugin
both the modules Plugin and Printer.  For some reason this two modules now
require that i explicitly open them in the source code, all the other
modules are working normally without the need to explicit opening them in
the source code.


2014-09-05 19:22 GMT+01:00 Claude Marche <Claude.Marche at inria.fr>:

>
>
> On 09/04/2014 09:40 PM, Jos? Pinheiro wrote:
>
>> Thank you very much Claude.
>>
>> I just had to change the whylib location but then it stopped giving
>> "Unbound Module Why3".
>>
>> Unfortunately, it seems to stopped working with frama-c modules:
>>
>> "Error: Unbound module Plugin.Register"
>>
>> Any ideia why?
>>
>
> Did you check that FRAMAC_LIBDIR and FRAMAC_SHARE are correct for your
> installation of Frama-C ?
>
> To get more help, you should send the compilation command that raises this
> error.
>
>
>>
>>
>>
>> 2014-09-04 19:45 GMT+01:00 Claude Marche <Claude.Marche at inria.fr
>> <mailto:Claude.Marche at inria.fr>>:
>>
>>
>>     Yes, one should be able to compile a Frama-C plugin using Why3 API.
>>     A Makefile of the following shape should work.
>>
>>     ------------------------------__---------------
>>     FRAMAC_SHARE  = /usr/local/share/frama-c
>>     FRAMAC_LIBDIR = /usr/local/lib/frama-c
>>
>>     PLUGIN_NAME     := <your plugin name>
>>     PLUGIN_CMO      := <your own codes as .cmo files>
>>
>>     SHELL := /bin/bash
>>
>>     WHYLIB := /use/local/lib/why3
>>
>>     PLUGIN_EXTRA_BYTE:= $(WHYLIB)/why3.cma
>>     PLUGIN_EXTRA_OPT:= $(WHYLIB)/why3.cmxa
>>     PLUGIN_BFLAGS:= -I $(WHYLIB)
>>     PLUGIN_OFLAGS:= -I $(WHYLIB)
>>     PLUGIN_LINK_BFLAGS:= -I $(WHYLIB)
>>     PLUGIN_LINK_OFLAGS:= -I $(WHYLIB)
>>     PLUGIN_TESTS_DIRS := <your test dirs>
>>
>>     $(addsuffix .cmo, $(PLUGIN_CMO)): $(WHYLIB)/why3.cmi
>>     $(addsuffix .cmx, $(PLUGIN_CMO)): $(WHYLIB)/why3.cmi
>> $(WHYLIB)/why3.cmx
>>
>>     include $(FRAMAC_SHARE)/Makefile.__dynamic
>>     ------------------------------__---------------------
>>
>>     - Claude
>>
>>
>>
>>
>>     On 09/04/2014 08:08 PM, Jos? Pinheiro wrote:
>>
>>         Hi, why3-club,
>>
>>         I would like to know if it is possible to use why3 api in a
>>         frama-c plugin.
>>         The problem it occurs, is the requirement to run why3 api with:
>>
>>           > ocamlc str.cma unix.cma nums.cma dynlink.cma -I +ocamlgraph
>>         -I +why3
>>         graph.cma why3.cma <file>
>>
>>         Without this options, it will give the error: Unbound Module
>>         Why3, as it
>>         is expected.
>>
>>         Is it possible to add this options to the frama-c plugin
>>         makefile, and
>>         use why3 api in a frama-c plugin?
>>
>>
>>         Thanks in advance!
>>         Jos? Pinheiro
>>
>>
>>         _________________________________________________
>>         Why3-club mailing list
>>         Why3-club at lists.gforge.inria.__fr
>>         <mailto:Why3-club at lists.gforge.inria.fr>
>>         http://lists.gforge.inria.fr/__cgi-bin/mailman/listinfo/
>> why3-__club
>>         <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club>
>>
>>     _________________________________________________
>>     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
>>     <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/
>> frama-c-discuss>
>>
>>
>>
>>
>> --
>> Cumprimentos,
>> Jos? Pinheiro
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>
>>  _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Cumprimentos,
Jos? Pinheiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140905/1c4e093e/attachment.html>