From cd81eaa6c5b3429f5535211040289a95ea25d4dc Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Tue, 22 Sep 2020 10:17:52 +0200 Subject: [PATCH] [eacsl] Add optional dependency to the Eva plugin --- src/plugins/e-acsl/.gitignore | 1 + src/plugins/e-acsl/Makefile.in | 51 ++++++++++++++++++- src/plugins/e-acsl/headers/header_spec.txt | 3 ++ .../src/dependencies/dep_eva.disabled.ml | 23 +++++++++ .../src/dependencies/dep_eva.enabled.ml | 23 +++++++++ .../e-acsl/src/dependencies/dep_eva.mli | 27 ++++++++++ 6 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml create mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml create mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.mli diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index f5ee39fdfac..5543dbdb43e 100644 --- a/src/plugins/e-acsl/.gitignore +++ b/src/plugins/e-acsl/.gitignore @@ -77,3 +77,4 @@ lib/libeacsl-rtl-bittree-dbg.a lib/libeacsl-rtl-segment-dbg.a tests/csrv14/* src/local_config.ml +src/dependencies/dep_eva.ml diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 3dbd78d2aee..aed90a086c6 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -44,6 +44,11 @@ SRC_LIBRARIES:= \ varname SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES)) +# source files that depend on optional dependencies +SRC_DYN_DEPENDENCIES:= \ + dep_eva +SRC_DYN_DEPENDENCIES:=$(addprefix src/dependencies/, $(SRC_DYN_DEPENDENCIES)) + # project initializer SRC_PROJECT_INITIALIZER:= \ rtl \ @@ -92,6 +97,7 @@ PLUGIN_DIR ?=. PLUGIN_EXTRA_DIRS:=\ src \ src/libraries \ + src/dependencies \ src/analyses \ src/project_initializer \ src/code_generator @@ -101,6 +107,7 @@ PLUGIN_NAME:=E_ACSL PLUGIN_CMO:= src/local_config \ src/options \ $(SRC_LIBRARIES) \ + $(SRC_DYN_DEPENDENCIES) \ $(SRC_PROJECT_INITIALIZER) \ $(SRC_ANALYSES) \ $(SRC_CODE_GENERATOR) \ @@ -109,6 +116,7 @@ PLUGIN_CMO:= src/local_config \ PLUGIN_HAS_MLI:=yes PLUGIN_DISTRIBUTED:=yes PLUGIN_DEPENDENCIES:= RteGen +PLUGIN_GENERATED:= # We "save" this variable so that it can be used once PLUGIN_DIR has been reset EACSL_PLUGIN_DIR:=$(PLUGIN_DIR) @@ -118,6 +126,46 @@ $(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmo \ $(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmi: E_ACSL_BFLAGS+= -w -60 $(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmx: E_ACSL_OFLAGS+= -w -60 +######################## +# Dynamic dependencies # +######################## + +# Distributed files for the dynamic dependencies +EACSL_DISTRIB_DYNDEP:= + +# Eva +DEP_EVA :=src/dependencies/dep_eva +DEP_EVA_ENABLED :=$(DEP_EVA).enabled.ml +DEP_EVA_DISABLED :=$(DEP_EVA).disabled.ml +PLUGIN_GENERATED += $(EACSL_PLUGIN_DIR)/$(DEP_EVA).ml + +## Add enabled and disabled files to the list of distributed files +## (relative to e-acsl directory) +EACSL_DISTRIB_DYNDEP += $(DEP_EVA_ENABLED) $(DEP_EVA_DISABLED) + +## Update enabled and disabled files path to be relative to the root directory +DEP_EVA_ENABLED:=$(addprefix $(EACSL_PLUGIN_DIR)/, $(DEP_EVA_ENABLED)) +DEP_EVA_DISABLED:=$(addprefix $(EACSL_PLUGIN_DIR)/, $(DEP_EVA_DISABLED)) + +## Add Eva to the plugin dependencies if enabled +ifneq "$(ENABLE_EVA)" "no" + PLUGIN_DEPENDENCIES+= Eva +endif + +## Copy enabled or disabled file to the source file that will be used for the +## compilation +$(EACSL_PLUGIN_DIR)/src/dependencies/dep_eva.ml: \ + $(DEP_EVA_ENABLED) $(DEP_EVA_DISABLED) \ + $(EACSL_PLUGIN_DIR)/Makefile share/Makefile.config + $(PRINT_MAKING) $@ + $(RM) $@ +ifneq "$(ENABLE_EVA)" "no" + $(CP) $(DEP_EVA_ENABLED) $@ +else + $(CP) $(DEP_EVA_DISABLED) $@ +endif + $(CHMOD_RO) $@ + ############### # Local Flags # ############### @@ -128,7 +176,7 @@ IS_DISTRIBUTED:=no # Local configuration # ####################### -PLUGIN_GENERATED:= $(EACSL_PLUGIN_DIR)/src/local_config.ml +PLUGIN_GENERATED += $(EACSL_PLUGIN_DIR)/src/local_config.ml VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION @@ -324,6 +372,7 @@ EACSL_MISC_FILES = \ EACSL_SHARE_FILES = share/e-acsl/*.[ch] share/e-acsl/*/*.[ch] EACSL_DISTRIB_EXTERNAL =\ + $(EACSL_DISTRIB_DYNDEP) \ $(EACSL_SHARE_FILES) \ $(EACSL_MISC_FILES) \ $(EACSL_DOC_FILES) \ diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index b08f8b18f34..de8c767ec75 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -116,6 +116,9 @@ src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/dependencies/dep_eva.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/dependencies/dep_eva.enabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/dependencies/dep_eva.disabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/libraries/builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/libraries/builtins.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/libraries/error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL diff --git a/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml b/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml new file mode 100644 index 00000000000..574d25ed1ab --- /dev/null +++ b/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +let use_builtin _ _ = () diff --git a/src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml b/src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml new file mode 100644 index 00000000000..a1af5ca1cb0 --- /dev/null +++ b/src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +let use_builtin = Eva.Value_parameters.use_builtin diff --git a/src/plugins/e-acsl/src/dependencies/dep_eva.mli b/src/plugins/e-acsl/src/dependencies/dep_eva.mli new file mode 100644 index 00000000000..a151c251eeb --- /dev/null +++ b/src/plugins/e-acsl/src/dependencies/dep_eva.mli @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +open Cil_types + +val use_builtin: kernel_function -> string -> unit +(** Call the function Eva.Value_parameters.use_builtin if Eva is enabled, + do nothing otherwise. *) -- GitLab