[eacsl] Add optional dependency to the Eva plugin

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

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) \

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

src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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 _ _ = ()

src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/e-acsl/src/dependencies/dep_eva.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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. *)