Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 06451607 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Integrate Jessie3 build into the primary Makefile.

parent 167477b6
Branches
Tags
No related merge requests found
......@@ -48,6 +48,7 @@ OCAMLVERSION = @OCAMLVERSION@
COQC = @COQC@
COQDEP = @COQDEP@
CAMLP5O = @CAMLP5O@
FRAMAC_LIBDIR = @FRAMAC_LIBDIR@
DEPFLAGS = -slash -I lib/why3
ifeq (@OCAMLBEST@,opt)
......@@ -1011,6 +1012,30 @@ opt byte: drivers/pvs-realizations.aux
clean::
rm -f drivers/pvs-realizations.aux
################
# Jessie3 plugin
################
ifeq (@enable_frama_c@,yes)
byte: jessie.byte
opt: jessie.opt
jessie.byte: lib/why3/why3.cma
@$(MAKE) -C src/jessie Jessie3.cma
jessie.opt: lib/why3/why3.cmxa
@$(MAKE) -C src/jessie Jessie3.cmxs
install_no_local::
mkdir -p $(FRAMAC_LIBDIR)/plugins/
cp -f src/jessie/Jessie3.cm* $(FRAMAC_LIBDIR)/plugins/
clean::
$(MAKE) -C src/jessie clean
endif
#######
# tools
#######
......
......@@ -113,6 +113,12 @@ AC_ARG_ENABLE(html-doc,
[ --enable-html-doc build HTML documentation],,
enable_html_doc=yes)
# Frama-C plugin
AC_ARG_ENABLE(frama-c,
[ --enable-frama-c enable Frama-C plugin],,
enable_frama_c=yes)
# profiling
AC_ARG_ENABLE(profiling,
......@@ -536,6 +542,29 @@ if test "$enable_hypothesis_selection" = yes; then
fi
fi
#check frama-c
if test "$enable_frama_c" = yes ; then
AC_CHECK_PROG(FRAMAC,frama-c,frama-c,no)
if test "$FRAMAC" = no ; then
AC_MSG_WARN(Cannot find Frama-C.)
enable_frama_c="no"
reason_frama_c=" (frama-c not found)"
else
AC_MSG_CHECKING(Frama-C version)
FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|Version: *\(.*\)$|\1|p'`
AC_MSG_RESULT($FRAMAC_VERSION)
case $FRAMAC_VERSION in
Oxygen-20120901) ;;
*) AC_MSG_WARN(Version Oxygen-20120901 required.)
enable_frama_c=no
reason_frama_c=" (version Oxygen required)"
;;
esac
FRAMAC_SHARE=`$FRAMAC -print-path`
FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
fi
fi
if test "$enable_local" = no; then
LOCALDIR=''
LOCALBIN=''
......@@ -617,6 +646,13 @@ AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)
AC_SUBST(enable_frama_c)
AC_SUBST(FRAMAC)
AC_SUBST(FRAMAC_VERSION)
AC_SUBST(FRAMAC_SHARE)
AC_SUBST(FRAMAC_LIBDIR)
AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)
AC_SUBST(LOCALBIN)
......@@ -676,6 +712,12 @@ if test "$enable_pvs_support" = yes ; then
echo " NASA libraries : $enable_pvs_nasa_libs$reason_pvs_nasa_libs"
fi
fi
echo "Frama-C support : $enable_frama_c$reason_frama_c"
if test "$enable_frama_c" = yes ; then
echo " Version : $FRAMAC_VERSION"
echo " Share path : $FRAMAC_SHARE"
echo " Library path : $FRAMAC_LIBDIR"
fi
echo "Hypothesis selection : $enable_hypothesis_selection"
if test "$enable_local" = yes ; then
echo "Installable : no"
......
FRAMAC_SHARE := $(shell frama-c -print-path)
FRAMAC_LIBDIR := $(shell frama-c -print-libpath)
FRAMAC_SHARE = @FRAMAC_SHARE@
FRAMAC_LIBDIR = @FRAMAC_LIBDIR@
PLUGIN_NAME := Jessie3
PLUGIN_CMO := literals ACSLtoWhy3 register
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment