Skip to content
Snippets Groups Projects
Commit 9c104b4e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Remove old configure inputs

parent 90cc3b21
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 744 deletions
src/plugins/aorai/configure.ac deleted 100644 → 0
+ 0
− 50
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Aorai plug-in of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# INRIA (Institut National de Recherche en Informatique et en #
# Automatique) #
# INSA (Institut National des Sciences Appliquees) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS],
[m4_include(FRAMAC_SHARE/configure.ac)]
)
check_plugin(aorai,PLUGIN_RELATIVE_PATH(plugin_file),[support for Aorai plug-in],yes)
plugin_use_external(aorai,ltltoba)
if test "$ENABLE_AORAI" != "no"; then
# ltl2ba library
configure_tool([LTLTOBA],[ltl2ba],[ltl2ba not found.],no)
fi
check_plugin_dependencies
write_plugin_config(Makefile)
src/plugins/dive/configure.ac deleted 100644 → 0
+ 0
− 51
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(dive,PLUGIN_RELATIVE_PATH(plugin_file),
[support for Dive plug-in],yes)
# Plug-in dependencies
######################
plugin_require(dive,eva)
plugin_require(dive,studia)
plugin_require(dive,server)
#plugin_use(dive,usable_plugin_but_not_mandatory)
check_plugin_dependencies
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/e-acsl/configure.ac deleted 100644 → 0
+ 0
− 101
View file @ 90cc3b21
##########################################################################
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2012-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
########################################
# E-ACSL as a standard Frama-C plug-in #
########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(e_acsl,PLUGIN_RELATIVE_PATH(plugin_file),
[support for E-ACSL plug-in],yes)
plugin_require(e_acsl,rtegen)
# E-ACSL only works on Linux as of now. Disable it on Mac OS and Windows
AC_CHECK_PROG(UNAME,uname,uname,no)
if test "$UNAME" = "no"; then
plugin_disable(e_acsl,[Not on a POSIX platform.])
fi
HOST_OS=$($UNAME -s)
case $HOST_OS in
Darwin | Linux | DragonFly | FreeBSD | NetBSD | OpenBSD)
# BSDs haven't really be tested, but it should at least compile fine
;;
*)
plugin_disable(e_acsl,[unsupported system $HOST_OS])
;;
esac
check_plugin_dependencies
###############################
# C specific stuff for E-ACSL #
###############################
MAY_RUN_TESTS=yes
# C compiler and stdio.h
#########################
AC_CHECK_HEADERS([stdio.h],[HAVE_STDIO_H=yes],)
# not sure it can actually happen:
# looks like configure stops on error if no C compiler detected
if test -z $HAVE_STDIO_H; then
MAY_RUN_TESTS=no
AC_MSG_WARN([stdio.h missing: non-regression tests unavailable.])
fi
# Doxygen
#########
AC_CHECK_PROG(DOXYGEN,doxygen,doxygen,no)
AC_CHECK_PROG(HAVE_DOT,dot,yes,no)
AC_OUTPUT(PLUGIN_RELATIVE_PATH(doc/doxygen/doxygen.cfg), [ ])
#######################
# Generating Makefile #
#######################
AC_SUBST(MAY_RUN_TESTS)
write_plugin_config(Makefile)
###############################
# Configure contrib libraries #
###############################
m4_ifndef([plugin_dir], [
m4_define([plugin_dir],[./])
])
src/plugins/instantiate/configure.ac deleted 100644 → 0
+ 0
− 45
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
##########################################
# Instantiate plugin #
##########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(instantiate,PLUGIN_RELATIVE_PATH(plugin_file),
[support for instantiate plug-in],yes)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/loop_analysis/configure.ac deleted 100644 → 0
+ 0
− 46
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
##############################################
# LoopAnalysis as a standard Frama-C plug-in #
##############################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(loop_analysis,PLUGIN_RELATIVE_PATH(plugin_file),
[support for loop analysis plug-in],yes)
plugin_require(loop_analysis,eva)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/markdown-report/configure.ac deleted 100644 → 0
+ 0
− 48
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS],
[m4_include(FRAMAC_SHARE/configure.ac)]
)
check_plugin(mdr,PLUGIN_RELATIVE_PATH(plugin_file),[Markdown/SARIF report plug-in],yes)
plugin_use(mdr,eva)
plugin_require_pkg(mdr,ppx_deriving)
plugin_require_pkg(mdr,ppx_deriving_yojson)
configure_pkg(ppx_deriving,[package ppx_deriving not found])
configure_pkg(ppx_deriving_yojson,[package ppx_deriving_yojson not found])
check_plugin_dependencies
write_plugin_config(Makefile)
src/plugins/nonterm/configure.ac deleted 100644 → 0
+ 0
− 47
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
########################################
# Nonterm as a standard Frama-C plug-in #
########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(nonterm,PLUGIN_RELATIVE_PATH(plugin_file),
[support for nonterm plug-in],yes)
plugin_require(nonterm,eva)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/obfuscator/configure.ac deleted 100644 → 0
+ 0
− 38
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS],
[m4_include(FRAMAC_SHARE/configure.ac)]
)
check_plugin(obfuscator,PLUGIN_RELATIVE_PATH(plugin_file),[support for Obfuscator plug-in],yes)
write_plugin_config(Makefile)
src/plugins/report/configure.ac deleted 100644 → 0
+ 0
− 45
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
########################################
# E-ACSL as a standard Frama-C plug-in #
########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(report,PLUGIN_RELATIVE_PATH(plugin_file),
[support for report plug-in],yes)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/security_slicing/configure.ac deleted 100644 → 0
+ 0
− 43
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS],[m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(security_slicing,PLUGIN_RELATIVE_PATH(plugin_file),
[support for Security_slicing plug-in],yes)
plugin_require(security_slicing,slicing)
plugin_require(security_slicing,eva)
plugin_require(security_slicing,pdg)
plugin_require(security_slicing,gui)
check_plugin_dependencies
write_plugin_config(Makefile)
src/plugins/server/configure.ac deleted 100644 → 0
+ 0
− 65
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
########################################
# Server as a standard Frama-C plug-in #
########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(server,PLUGIN_RELATIVE_PATH(plugin_file),[Server plug-in],yes)
########################################
# Server ZMQ Configuration #
########################################
AC_ARG_ENABLE(
server-zmq,
[ --enable-server-zmq Server ZeroMQ support (default: yes)],
SERVER_ZMQ=$enableval,
SERVER_ZMQ=yes
)
if test "$SERVER_ZMQ" = "yes" ;
then
configure_pkg([zmq],
[Server support for ZeroMQ disabled (try 'opam install zmq').])
plugin_use_pkg(server,zmq)
SERVER_ZMQ=$HAS_OCAML_ZMQ
fi
AC_SUBST(SERVER_ZMQ)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/studia/configure.ac deleted 100644 → 0
+ 0
− 48
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
########################################
# Studia as a standard Frama-C plug-in #
########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(studia,PLUGIN_RELATIVE_PATH(plugin_file),
[support for studia plug-in],yes)
plugin_require(studia,eva)
plugin_require(studia,server)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/variadic/configure.ac deleted 100644 → 0
+ 0
− 45
View file @ 90cc3b21
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
##########################################
# Variadic as a standard Frama-C plug-in #
##########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(variadic,PLUGIN_RELATIVE_PATH(plugin_file),
[support for variadic plug-in],yes)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
src/plugins/wp/configure.ac deleted 100644 → 0
+ 0
− 72
View file @ 90cc3b21
##########################################################################
# #
# This file is part of WP plug-in of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat a l'energie atomique et aux energies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS],
[m4_include(FRAMAC_SHARE/configure.ac)]
)
check_plugin(wp,PLUGIN_RELATIVE_PATH(plugin_file),[WP plug-in],yes,yes)
plugin_require(wp,qed)
plugin_require(wp,rtegen)
plugin_use(wp,gui)
# Why3 API dependency
######################
configure_pkg(why3,[package why3 not found])
plugin_require_pkg(wp,why3)
check_plugin_dependencies
if test "$HAS_OCAML_WHY3" = "yes"; then
AC_MSG_CHECKING(why3 version)
WHY3VERSION=`ocamlfind query -format %v why3 | tr -d '\\r\\n'`
case $WHY3VERSION in
"")
AC_MSG_RESULT([not found!])
plugin_disable(wp,[why3 not found])
;;
0.* | 1.[[01234]].*)
AC_MSG_RESULT([found $WHY3VERSION: requires 1.5.0+])
plugin_disable(wp,[non-supported why3 $WHY3VERSION])
;;
1.5.*)
AC_MSG_RESULT([found $WHY3VERSION: ok])
;;
*)
AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.5.0+)])
;;
esac
fi
write_plugin_config(Makefile)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment