diff --git a/configure.in b/configure.in index 8abb2c187883030699165ae9ed9efa9ae3cca7dc..e5bd40a6513a1d657def0d283f009bb05147adaa 100644 --- a/configure.in +++ b/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 diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 2f826961dbc5ba32495c8d1660baa1890f6cd291..8400bc0b75b7c5909a1637aec9185fdd562ded33 100644 --- a/headers/header_spec.txt +++ b/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 diff --git a/src/plugins/studia/.gitignore b/src/plugins/studia/.gitignore index 3e06586e47075d14472acd28c7d10e2392a4159d..70edc7aaf5d8a94a495a3bda78751d22ea6b055a 100644 --- a/src/plugins/studia/.gitignore +++ b/src/plugins/studia/.gitignore @@ -1,13 +1,3 @@ -*~ -*.cm* -*.annot -*.o -*_DEP -local_config.ml -.depend +/Makefile /tests/ptests_config -result -/gui -/top -/.Makefile.plugin.generated -/Studia.check_mli_exists +/tests/nonterm/result diff --git a/src/plugins/studia/Makefile.in b/src/plugins/studia/Makefile.in new file mode 100644 index 0000000000000000000000000000000000000000..8fed39590fc74c44ecef66242a547a34380c5cdd --- /dev/null +++ b/src/plugins/studia/Makefile.in @@ -0,0 +1,64 @@ +########################################################################## +# # +# 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 $@ diff --git a/src/plugins/studia/Makefile b/src/plugins/studia/configure.ac similarity index 71% rename from src/plugins/studia/Makefile rename to src/plugins/studia/configure.ac index b7665d764aa3b3bd662493144754cf2d67af457c..08d83084ebda36f31492a04e66a750243e73e500 100644 --- a/src/plugins/studia/Makefile +++ b/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)