Merge branch 'fix/andre/configure-disable-eva' into 'master'

[configure] fix dependencies on Eva plugin; standardize Studia plugin

Closes #634

See merge request frama-c/frama-c!2220

configure.in

@@ -774,7 +774,7 @@ plugin_require(inout,callgraph)
 #########
 
 check_plugin(metrics,src/plugins/metrics,[support for metrics analysis],yes)
-plugin_use(metrics,eva)
+plugin_require(metrics,eva)
 plugin_use(metrics,gui)
 
 # occurrence

headers/header_spec.txt

@@ -1073,7 +1073,8 @@ src/plugins/sparecode/spare_marks.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/sparecode/sparecode_params.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/sparecode/sparecode_params.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/sparecode/transform.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/Makefile: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/configure.ac: CEA_LGPL_OR_PROPRIETARY
 src/plugins/studia/options.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/studia/options.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/studia/reads.ml: CEA_LGPL_OR_PROPRIETARY

src/plugins/loop_analysis/.gitignore

+/configure
 /Makefile
 /tests/ptests_config
 /tests/*/result

src/plugins/nonterm/.gitignore

+/configure
 /Makefile
 /tests/ptests_config
-/tests/nonterm/result
+/tests/*/result

src/plugins/obfuscator/.gitignore

+/configure
 /Makefile
 /tests/ptests_config
 /tests/*/result

src/plugins/report/.gitignore

+/configure
 /Makefile
 /tests/ptests_config
-/tests/report/result
+/tests/*/result

src/plugins/studia/.gitignore

-*~
-*.cm*
-*.annot
-*.o
-*_DEP
-local_config.ml
-.depend
+/configure
+/Makefile
 /tests/ptests_config
-result
-/gui
-/top
-/.Makefile.plugin.generated
-/Studia.check_mli_exists
+/tests/*/result

src/plugins/studia/Makefile.in

+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2019                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+# Do not use ?= to initialize both below variables
+# (fixed efficiency issue, see GNU Make manual, Section 8.11)
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
+endif
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
+endif
+
+###################
+# Plug-in Setting #
+###################
+
+PLUGIN_DIR ?=.
+PLUGIN_ENABLE:=@ENABLE_STUDIA@
+PLUGIN_NAME:=Studia
+PLUGIN_CMO:= options writes reads
+PLUGIN_GUI_CMO:= studia_gui
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_DEPENDENCIES:=Eva
+PLUGIN_NO_TEST:=no
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR=$(FRAMAC_SRC)
+else
+CONFIG_STATUS_DIR=.
+endif
+
+$(Studia_DIR)/Makefile: $(Studia_DIR)/Makefile.in \
+                         $(CONFIG_STATUS_DIR)/config.status
+	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/studia/Makefile → src/plugins/studia/configure.ac

@@ -20,31 +20,28 @@
 #                                                                        #
 ##########################################################################
 
-#######################
-# Frama-C Environment #
-#######################
+########################################
+# Studia as a standard Frama-C plug-in #
+########################################
+
+m4_define([plugin_file],Makefile.in)
 
-ifndef FRAMAC_SHARE
-FRAMAC_SHARE	:= $(shell frama-c-config -print-share-path)
-endif
+m4_define([FRAMAC_SHARE_ENV],
+          [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
 
-ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR	:= $(shell frama-c-config -print-libpath)
-endif
+m4_define([FRAMAC_SHARE],
+          [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+                                     [m4_esyscmd(frama-c -print-path)])])
 
-#########################
-# Plug-in configuration #
-#########################
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
 
-PLUGIN_DIR ?=.
-PLUGIN_NAME:=Studia
-PLUGIN_CMO:=options writes reads
-PLUGIN_GUI_CMO:=studia_gui
-PLUGIN_DEPENDENCIES:=Eva
-PLUGIN_DISTRIB_EXTERNAL:= Makefile
+check_plugin(studia,PLUGIN_RELATIVE_PATH(plugin_file),
+             [support for studia plug-in],yes)
 
-################
-# Generic part #
-################
+plugin_require(studia,eva)
+
+#######################
+# Generating Makefile #
+#######################
 
-include $(FRAMAC_SHARE)/Makefile.dynamic
+write_plugin_config(Makefile)

src/plugins/variadic/.gitignore

+/configure
 /Makefile
 /tests/ptests_config
 /tests/*/result