diff --git a/Makefile b/Makefile index baf54d81140ef1b2dc33c065060e4938b7d2c313..310df6be813458feab212edff6ca70b2114d9021 100644 --- a/Makefile +++ b/Makefile @@ -51,9 +51,6 @@ else OPTDOT=None endif -ALL_LIBRARY_NAMES=$(shell ocamlfind query -r -p-format $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI)) \ - frama-c.init frama-c.kernel frama-c.gui - ifeq ($(HAS_OCAML408),yes) DYNLINK_INIT=fun () -> () FORMAT_STAG=stag @@ -107,7 +104,6 @@ config.sed: VERSION share/Makefile.config Makefile configure.in @echo "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" >> $@ @echo "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" >> $@ @echo "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" >> $@ - @echo "s|@LIBRARY_NAMES@|$(foreach p,$(ALL_LIBRARY_NAMES),\"$p\";)|" >> $@ @echo "s|@OPTDOT@|$(OPTDOT)|" >> $@ @echo "s|@EXE@|$(EXE)|" >> $@ @echo "s/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g" >> $@ @@ -130,12 +126,6 @@ clean: dune clean rm -rf _build .merlin config.sed -%.cmxs: %.ml - dune exec -- ocamlfind ocamlopt -package frama-c.kernel -open Frama_c_kernel -shared -o $@ $< - -%.o: %.ml - dune exec -- ocamlfind ocamlopt -package frama-c.kernel -open Frama_c_kernel -c -o $@ $< - ######################################################################## # Makefile.config is rebuilt whenever configure.in is modified # ######################################################################## diff --git a/configure.in b/configure.in index aa745f3592c87a2d629dddc80894fbc71790a446..3918eb98726aa4f41acbf014376f0340fb090659 100644 --- a/configure.in +++ b/configure.in @@ -195,12 +195,11 @@ fi # checking for ocamlfind -AC_CHECK_PROG(OCAMLFIND,ocamlfind,ocamlfind,no) -if test "$OCAMLFIND" != no ; then - OCAMLC="$OCAMLFIND ocamlc" - OCAMLOPT="$OCAMLFIND ocamlopt" +AC_CHECK_PROG(DUNE,dune,dune,no) +if test "$DUNE" != no ; then + true else - AC_MSG_ERROR(Cannot find ocamlfind.) + AC_MSG_ERROR(Cannot find dune.) fi ################################################### @@ -230,172 +229,31 @@ else AC_MSG_NOTICE(Distribution mode: all warnings are deactivated) fi -############################################## -# Check for other mandatory tools/libraries # -############################################## - -new_section "configure mandatory tools and libraries" - -# ocamldep -AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no) -if test "$OCAMLDEP" = no ; then - AC_MSG_ERROR(Cannot find ocamldep.) -else - OCAMLDEP="$OCAMLFIND ocamldep" -fi - -# ocamllex -AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no) -if test "$OCAMLLEX" = no ; then - AC_MSG_ERROR(Cannot find ocamllex.) -else - AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no) - if test "$OCAMLLEXDOTOPT" != no ; then - OCAMLLEX=$OCAMLLEXDOTOPT - fi -fi - -# ocamlyacc -AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no) -if test "$OCAMLYACC" = no ; then - AC_MSG_ERROR(Cannot find ocamlyacc.) -fi - -# ocamlcp -AC_CHECK_PROG(OCAMLCP,ocamlcp,ocamlcp,no) -if test "$OCAMLCP" = no ; then - AC_MSG_ERROR(Cannot find ocamlcp.) -else - OCAMLCP="$OCAMLFIND ocamlcp" -fi - -# ocamlgraph -############ - -AC_MSG_CHECKING(for ocamlgraph) - -OCAMLGRAPH=$($OCAMLFIND query ocamlgraph -format %v) -if test -z "$OCAMLGRAPH" ; then - AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \ -(requires ocamlgraph 1.8.5 or higher).) -fi -case $OCAMLGRAPH in - 0.* | 1.[[01234567]].* \ - | 1.8.0 | 1.8.0+dev \ - | 1.8.1 | 1.8.1+dev \ - | 1.8.2 | 1.8.2+dev \ - | 1.8.3 | 1.8.3+dev \ - | 1.8.4 | 1.8.4+dev) - AC_MSG_ERROR(found $OCAMLGRAPH: requires 1.8.5 or higher.);; - 1.8.5 | 1.8.6 | 1.8.7) - AC_MSG_RESULT(found);; - *) - AC_MSG_RESULT(found $OCAMLGRAPH: should work);; -esac - -# zarith -######## - -AC_MSG_CHECKING(for zarith) - -ZARITH=$($OCAMLFIND query zarith -format %v) -if test -z "$ZARITH" ; then - AC_MSG_ERROR(Cannot find zarith via ocamlfind (requires zarith 1.5 or higher).) -fi -case ZARITH in - 1.[[01234]].*) - AC_MSG_ERROR(found $ZARITH: requires 1.5 or higher.);; - *) - AC_MSG_RESULT(found $ZARITH);; -esac - -# yojson -######## - -AC_MSG_CHECKING(for Yojson) - -YOJSON=$($OCAMLFIND query yojson -format %v) -if test -z "$YOJSON" ; then - AC_MSG_ERROR(Cannot find yojson via ocamlfind \ -(requires yojson 1.4.1 or higher).) -else - AC_MSG_RESULT(found $YOJSON) -fi - -################################################# -# Check for other (optional) tools/libraries # -################################################# - -new_section "configure optional tools and libraries" - -AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,no) -if test "$OCAMLDOC" = no ; then - AC_MSG_RESULT(ocamldoc discarded not present) -else - OCAMLDOC="$OCAMLFIND ocamldoc" -fi - -AC_CHECK_PROG(OCAMLMKTOP,ocamlmktop,ocamlmktop,no) -if test "$OCAMLMKTOP" = no ; then - AC_MSG_RESULT(Cannot find ocamlmktop: toplevels cannot be built.) -else - OCAMLMKTOP="$OCAMLFIND ocamlmktop" -fi - -AC_CHECK_PROG(OTAGS,otags,otags,) - -# apron -######## - -AC_MSG_CHECKING(for Apron) - -APRON_PATH=$($OCAMLFIND query apron 2>/dev/null | tr -d '\r\n') -if test -f "$APRON_PATH/apron.$DYN_SUFFIX"; then - HAS_APRON="yes"; - AC_MSG_RESULT(found) -else - HAS_APRON="no"; - AC_MSG_RESULT(not found. The corresponding domains won't be available in Eva) -fi; - -# mpfr -####### - -AC_MSG_CHECKING(for MPFR) - -MPFR_PATH=$($OCAMLFIND query gmp 2>/dev/null | tr -d '\r\n') -if test -f "$MPFR_PATH/gmp.$DYN_SUFFIX" -a -f "$MPFR_PATH/mpfr.cmx" ; then - HAS_MPFR="yes"; - AC_MSG_RESULT(found) -else - HAS_MPFR="no"; - AC_MSG_RESULT(not found. The numerors domain won't be available in Eva) -fi; # landmarks (profiling tool, for developers) ######## -AC_ARG_ENABLE( - landmarks, - [ --enable-landmarks enable landmarks profiling (default: yes if package installed)], - ENABLE_LANDMARKS=$enableval, - ENABLE_LANDMARKS=yes) - -if test "$ENABLE_LANDMARKS" = yes ; then - AC_MSG_CHECKING(for Landmarks) - LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n') - LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n') - if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then - HAS_LANDMARKS="yes"; - AC_MSG_RESULT(found) - else - HAS_LANDMARKS="no"; - AC_MSG_RESULT(not found.) - fi; -else - AC_MSG_RESULT(Landmarks profiling disabled); - HAS_LANDMARKS="no" -fi +dnl AC_ARG_ENABLE( +dnl landmarks, +dnl [ --enable-landmarks enable landmarks profiling (default: yes if package installed)], +dnl ENABLE_LANDMARKS=$enableval, +dnl ENABLE_LANDMARKS=yes) + +dnl if test "$ENABLE_LANDMARKS" = yes ; then +dnl AC_MSG_CHECKING(for Landmarks) +dnl LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n') +dnl LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n') +dnl if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then +dnl HAS_LANDMARKS="yes"; +dnl AC_MSG_RESULT(found) +dnl else +dnl HAS_LANDMARKS="no"; +dnl AC_MSG_RESULT(not found.) +dnl fi; +dnl else +dnl AC_MSG_RESULT(Landmarks profiling disabled); +dnl HAS_LANDMARKS="no" +dnl fi ############ # Platform # @@ -634,320 +492,6 @@ CPPFLAGS=$OLD_CPPFLAGS AC_MSG_RESULT(Default preprocessor supported architecture-related options: $DEFAULT_CPP_SUPPORTED_ARCH_OPTS) - -################# -# Plugin wished # -################# - -new_section "wished frama-c plug-ins" - -# Option -with-no-plugin -####################### - -define([NO_PLUGIN_HELP], - AC_HELP_STRING([--with-no-plugin], - [disable all plug-ins (default: no)])) - -AC_ARG_WITH(no-plugin,NO_PLUGIN_HELP,[ONLY_KERNEL=$withval],[ONLY_KERNEL=no]) - -# library declarations -###################### - -# REQUIRE_LIBRARY: library *must* be present in order to build plugins -# USE_LIBRARY: better for plugins if library is present, but not required -# HAS_LIBRARY: is the library available? - -REQUIRE_LABLGTK= -USE_LABLGTK= -HAS_LABLGTK= - -### Now plugin declarations - -PLUGINS_FORCE_LIST= - -############################################################################### -# # -#################### # -# Plug-in sections # # -#################### # -# # -# For 'internal' developers: # -# Add your own plug-in here # -# # -############################################################################### - -# callgraph -########### - -check_plugin(callgraph, src/plugins/callgraph, - [support for callgraph plugin], yes) - -plugin_use_external(callgraph,dot) -plugin_use(callgraph,gui) -plugin_use(callgraph,eva) - -# constant propagation -###################### - -check_plugin(semantic_constant_folding, src/plugins/constant_propagation, - [support for constant propagation plugin],yes) - -plugin_require(semantic_constant_folding,eva) - -# from -###### - -check_plugin(from_analysis,src/plugins/from,[support for from analysis],yes) - -plugin_require(from_analysis,eva) -plugin_require(from_analysis,callgraph) - -# gui -##### - -check_plugin(gui,src/plugins/gui,[support for gui],yes) - -plugin_require_external(gui,lablgtk) -plugin_use_external(gui,gnomecanvas) -plugin_require_external(gui,gtksourceview) -plugin_use_external(gui,dot) - -# impact -######## - -check_plugin(impact,src/plugins/impact,[support for impact plugin],yes) - -plugin_use(impact,gui) -plugin_use(impact,slicing) -plugin_require(impact,pdg) -plugin_require(impact,eva) -plugin_require(impact,inout) - -# inout -####### - -check_plugin(inout,src/plugins/inout,[support for inout analysis],yes) -plugin_require(inout,from_analysis) -plugin_require(inout,eva) -plugin_require(inout,callgraph) - -# metrics -######### - -check_plugin(metrics,src/plugins/metrics,[support for metrics analysis],yes) -plugin_require(metrics,eva) -plugin_use(metrics,gui) - -# occurrence -############ - -check_plugin(occurrence,src/plugins/occurrence, - [support for occurrence analysis],yes) -plugin_use(occurrence,gui) -plugin_require(occurrence,eva) - -# pdg -##### - -check_plugin(pdg,src/plugins/pdg,[support for pdg plugin],yes,pdg_types) -plugin_require(pdg,from_analysis) -plugin_require(pdg,eva) -plugin_require(pdg,callgraph) - -# postdominators -################ - -check_plugin(postdominators,src/plugins/postdominators, - [support for postdominators plugin],yes) - -# rte -##### - -check_plugin(rtegen,src/plugins/rte, - [support for runtime error annotation],yes) - -# scope -############ - -check_plugin(scope,src/plugins/scope,[support for scope plugin],yes) -plugin_require(scope,postdominators) -plugin_require(scope,eva) -plugin_require(scope,from_analysis) -plugin_require(scope,pdg) -plugin_use(scope,gui) - -# slicing -######### - -check_plugin(slicing,src/plugins/slicing,[support for slicing plugin],yes) -plugin_require(slicing,from_analysis) -plugin_require(slicing,pdg) -plugin_require(slicing,eva) -plugin_require(slicing,callgraph) -plugin_use(slicing,gui) - -# spare code -############ - -check_plugin(sparecode,src/plugins/sparecode, - [support for sparecode plugin],yes) -plugin_require(sparecode,pdg) -plugin_require(sparecode,eva) - -# users -####### - -check_plugin(users,src/plugins/users,[support for users analysis],yes) -plugin_require(users,eva) -plugin_use(users,callgraph) - -# value -####### - -check_plugin(eva,src/plugins/value, - [support for value analysis],yes) -plugin_use(eva,gui) -plugin_use(eva,scope) -plugin_use(eva,callgraph) - -#################### -# External plugins # -#################### - -EXTRA_EXTERNAL_PLUGINS= - -AC_ARG_ENABLE(external, -[[ --enable-external=plugin - allows to compile directly from Frama-C kernel - some external plug-ins.]], -[ - for dir in $enableval; do - if test -d $dir; then - AC_MSG_NOTICE([external plug-in $dir found.]) - EXTRA_EXTERNAL_PLUGINS="$EXTRA_EXTERNAL_PLUGINS $dir" - olddir=$(pwd) - cd $dir; - if test -x ./configure; then - new_section "configure plug-in $dir" - ./configure --prefix=$prefix --datarootdir=$datarootdir \ - --exec_prefix=$exec_prefix --bindir=$bindir --libdir=$datadir/frama-c \ - --host=$host --build=$build --mandir=$mandir \ - || \ - AC_MSG_ERROR([cannot configure requested external plugin in $dir]) - fi; - cd $olddir - else - AC_MSG_ERROR([--enable-external expects an existing directory as argument.]) - fi; - done -]) - -AC_FOREACH([__plugin],m4_esyscmd([ls src/plugins]), - [ m4_if(m4_bregexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1], - [ - m4_define([plugin_dir],[src/plugins/__plugin]) - m4_syscmd(test -r plugin_dir/configure.in) - m4_define([is_configure_in],m4_sysval) - m4_syscmd(test -r plugin_dir/configure.ac) - m4_define([is_configure_ac],m4_sysval) - m4_define([config_file], - [m4_if(is_configure_in,0,plugin_dir/configure.in, - m4_if(is_configure_ac,0,plugin_dir/configure.ac,no))]) - m4_if(config_file,[no], - [ m4_syscmd(test -r plugin_dir/Makefile) - m4_if(m4_sysval,[0], - [ m4_syscmd(test "$DISTRIB_CONF" = "yes" && \ - grep -q -e "PLUGIN_DISTRIBUTED *:= *no" \ - plugin_dir/Makefile - ) - m4_if(m4_sysval,[0],, - [ check_plugin(__plugin,plugin_dir, - [support for __plugin plug-in],yes) - if test "$[ENABLE_]tovarname(__plugin)" != "no"; then - EXTERNAL_PLUGINS="$EXTERNAL_PLUGINS plugin_dir"; - fi])])], - [ m4_syscmd(test "$DISTRIB_CONF" = "yes" && \ - grep -q -e "PLUGIN_DISTRIBUTED:=no" \ - plugin_dir/Makefile.in) - m4_if(m4_sysval,[0],, - [ m4_define([plugin_prefix],plugin_dir) - m4_include(config_file) - m4_syscmd(cd plugin_dir && \ - [FRAMAC_SHARE]=../../../share autoconf)]) - ]) - m4_undefine([plugin_dir]) - ]) - ]) - -##################################################### -# Check for tools/libraries requirements of plugins # -##################################################### - -new_section "configure tools and libraries used by some plug-ins" - -# lablgtk2 -########## - -define([ENABLE_LABLGTK3_HELP], - AC_HELP_STRING([--disable-lablgtk3], - [in case lablgtk2 and lablgtk3 are available, the default is to compile - against lablgtk3. Use this option to force compiling against lablgtk2])) - -AC_ARG_ENABLE( - lablgtk3,[ENABLE_LABLGTK3_HELP], - [ENABLE_LABLGTK3=$enableval],[ENABLE_LABLGTK3=yes]) - -REQUIRE_LABLGTK="$REQUIRE_LABLGTK$REQUIRE_GNOMECANVAS" -USE_LABLGTK="$USE_LABLGTK$USE_GNOMECANVAS" - -LABLGTK_PATH="" -SOURCEVIEW_PATH="" - -if test "$PLATFORM" != "MacOS"; then -if test "$ENABLE_LABLGTK3" = "yes"; then - LABLGTK_PATH=`ocamlfind query lablgtk3 | tr -d '\\r\\n'`; -fi -if test "$LABLGTK_PATH" != ""; then - SOURCEVIEW_PATH=`ocamlfind query lablgtk3-sourceview3 | tr -d '\\r\\n'`; -fi -fi - -if test "$SOURCEVIEW_PATH" = ""; then - LABLGTK_VERSION=2 - LABLGTK_PATH=`ocamlfind query lablgtk2 | tr -d '\\r\\n'` - if test "$LABLGTK_PATH" = "" -o \ - "$LABLGTK_PATH" -ef "$OCAMLLIB/lablgtk2" ; then - echo "Ocamlfind -> using +lablgtk2.($LABLGTK_PATH,$OCAMLLIB/lablgtk2)" - LABLGTK_PATH=+lablgtk2 - LABLGTKPATH_FOR_CONFIGURE=$OCAMLLIB/lablgtk2 - else - echo "Ocamlfind -> using $LABLGTK_PATH" - LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH - fi; - SOURCEVIEW_PATH=$LABLGTKPATH_FOR_CONFIGURE; -else - LABLGTK_VERSION=3 - echo "ocamlfind -> using $LABLGTK_PATH" - LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH; -fi - -configure_library([GTKSOURCEVIEW], - [$SOURCEVIEW_PATH/lablgtksourceview2.$LIB_SUFFIX, - $SOURCEVIEW_PATH/lablgtk3_sourceview3.$LIB_SUFFIX], - [lablgtksourceview not found], - no) - -configure_library([GNOMECANVAS], - [$LABLGTKPATH_FOR_CONFIGURE/lablgnomecanvas.$LIB_SUFFIX], - [lablgnomecanvas.$LIB_SUFFIX not found], - no) - -configure_library([LABLGTK], - [$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX, - $LABLGTKPATH_FOR_CONFIGURE/lablgtk3.$LIB_SUFFIX], - [$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.], - no) - # dot and xdot tools #################### @@ -958,14 +502,6 @@ configure_tool([UNIX2DOS],[unix2dos], plugin_use_external(tests,unix2dos) -######################## -# Plug-in dependencies # -######################## - -new_section "checking for plug-in dependencies" - -check_frama_c_dependencies - ############################ # Substitutions to perform # ############################ @@ -1028,20 +564,4 @@ AC_OUTPUT() new_section "summary: plug-ins available" -for plugin in m4_flatten(PLUGINS_LIST); do - n=NAME_$plugin - e=ENABLE_$plugin - i=INFO_$plugin - eval nv=\$$n - eval ev=\$$e - eval iv=\$$i - AC_MSG_NOTICE([$nv: $ev$iv]) -done - -if test "$EXTRA_EXTERNAL_PLUGINS" != ""; then - new_section "summary: requested external plugins" -fi - -for plugin in $EXTRA_EXTERNAL_PLUGINS; do - AC_MSG_NOTICE([$plugin]) -done +$DUNE build -j1 --display quiet @frama-c-configure diff --git a/src/dune b/src/dune index 71ff17d8ddf65aa05232bf24dd10d700c9e0a8fc..76932bc363e25a2ab211029ff5d146dacf2e871c 100644 --- a/src/dune +++ b/src/dune @@ -1,3 +1,20 @@ +(rule + (alias frama-c-configure) + (deps (universe)) + (action (progn + (echo "Frama-C:" %{lib-available:frama-c.kernel} "\n") + (echo " - str:" %{lib-available:str} "\n") + (echo " - unix:" %{lib-available:unix} "\n") + (echo " - zarith:" %{lib-available:zarith} "\n") + (echo " - ocamlgraph:" %{lib-available:ocamlgraph} "\n") + (echo " - dynlink:" %{lib-available:dynlink} "\n") + (echo " - bytes:" %{lib-available:bytes} "\n") + (echo " - yojson:" %{lib-available:yojson} "\n") + (echo " - dune-site.plugins:" %{lib-available:dune-site.plugins} "\n") + ) + ) +) + (library (name frama_c_kernel) (public_name frama-c.kernel) diff --git a/src/plugins/gui/dune b/src/plugins/gui/dune index 7cb1ff502e0dab6277a2db8ee4c322127474d52f..0840c6b9fc031b8d6fcce42a69e247cc4e66cf71 100644 --- a/src/plugins/gui/dune +++ b/src/plugins/gui/dune @@ -1,3 +1,17 @@ +(rule + (alias frama-c-configure) + (deps (universe)) + (action (progn + (echo "GUI:" %{lib-available:frama-c.gui} "\n") + (echo " - lablgtk2:" %{lib-available:lablgtk2} "\n") + (echo " - lablgtk2.gnomecanvas:" %{lib-available:lablgtk2.gnomecanvas} "\n") + (echo " - lablgtk2.sourceview2:" %{lib-available:lablgtk2.sourceview2} "\n") + (echo " - lablgtk3:" %{lib-available:lablgtk3} "\n") + (echo " - lablgtk3-sourceview3:" %{lib-available:lablgtk3-sourceview3} "\n") + ) + ) +) + ( library (name frama_c_gui) (public_name frama-c.gui) diff --git a/src/plugins/markdown-report/dune b/src/plugins/markdown-report/dune index 0be220a665f59588b166f60bb7bad88e9717e6d1..a30c835400ec4f8dd7d963fdb71b07efda2c91e4 100644 --- a/src/plugins/markdown-report/dune +++ b/src/plugins/markdown-report/dune @@ -1,3 +1,13 @@ +(rule + (alias frama-c-configure) + (deps (universe)) + (action (progn + (echo "markdown-report:" %{lib-available:frama-c-markdown-report.core} "\n") + (echo " - ppx_deriving_yojson:" %{lib-available:ppx_deriving_yojson} "\n") + ) + ) +) + ( library (name markdown_report) (public_name frama-c-markdown-report.core) diff --git a/src/plugins/value/dune b/src/plugins/value/dune index 68f3533d98e3aa2e4056010adc0ca1df9c0efd35..bddc8130a80c8ccaa2850efcc2897d014575d465 100644 --- a/src/plugins/value/dune +++ b/src/plugins/value/dune @@ -1,3 +1,19 @@ +(rule + (alias frama-c-configure) + (deps (universe)) + (action (progn + (echo "EVA:" %{lib-available:frama-c-eva.core} "\n") + (echo "Numerors:" %{lib-available:frama-c-eva.numerors} "\n") + (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n") + (echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n") + (echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n") + (echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n") + (echo " - apron.polkaMPQ:" %{lib-available:apron.polkaMPQ} "\n") + (echo " - apron.apron:" %{lib-available:apron.apron} "\n") + ) + ) +) + ( library (name eva) (public_name frama-c-eva.core)