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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Fri, 05 Sep 2014 20:22:16 +0200
  • In-reply-to: <CAM1QBJPA65qKmKLMP3=qdRrX=5ncdRiWu9fYPgHabKrADPpHig@mail.gmail.com>
  • References: <CAM1QBJPSxOFR_XFUxaUmoyso-_kZDP6ZBLeN-ytmTaVEEuBiMA@mail.gmail.com> <5408B32C.70704@inria.fr> <CAM1QBJPA65qKmKLMP3=qdRrX=5ncdRiWu9fYPgHabKrADPpHig@mail.gmail.com>

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
>