diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index f5ee39fdfacb148fe2e6ab6c724865925290ea92..5543dbdb43e12ae58f5c6ecfa2674b7ebf5243c4 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 3dbd78d2aeee3a90b7c983dfb8f90b94482fc708..aed90a086c6ad3694d8b651b1b7c6dcb094c1d74 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 b08f8b18f343605bc1e665a58838130fd0ad8ca7..de8c767ec7536bab5ed0794cd0055c093ec1a9b0 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 0000000000000000000000000000000000000000..574d25ed1ab97726b75bbc3171c80783c81da567 --- /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 0000000000000000000000000000000000000000..a1af5ca1cb0ee3d51fb0b83bd2cdbf9c9bdb0ba2 --- /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 0000000000000000000000000000000000000000..a151c251eeb62727b283355f458cbbf03a5efb04 --- /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. *)