--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on September 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] Using Why3 api in frama-c plugin



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>