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: Thu, 04 Sep 2014 20:45:00 +0200
  • In-reply-to: <CAM1QBJPSxOFR_XFUxaUmoyso-_kZDP6ZBLeN-ytmTaVEEuBiMA@mail.gmail.com>
  • References: <CAM1QBJPSxOFR_XFUxaUmoyso-_kZDP6ZBLeN-ytmTaVEEuBiMA@mail.gmail.com>
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
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>