From 8a55809d798355f2ef7eee845f9111974cfd847e Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Tue, 25 May 2021 17:08:20 +0200 Subject: [PATCH] [eacsl] Remove optional dependency to Eva --- src/plugins/e-acsl/Makefile.in | 48 ------------------- .../src/dependencies/dep_eva.disabled.ml | 23 --------- .../src/dependencies/dep_eva.enabled.ml | 23 --------- .../e-acsl/src/dependencies/dep_eva.mli | 27 ----------- 4 files changed, 121 deletions(-) delete mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml delete mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml delete mode 100644 src/plugins/e-acsl/src/dependencies/dep_eva.mli diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 83c4a7647cb..cf4b2d96fba 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -48,11 +48,6 @@ 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 \ @@ -108,7 +103,6 @@ PLUGIN_DIR ?=. PLUGIN_EXTRA_DIRS:=\ src \ src/libraries \ - src/dependencies \ src/analyses \ src/project_initializer \ src/code_generator @@ -118,7 +112,6 @@ PLUGIN_NAME:=E_ACSL PLUGIN_CMO:= src/local_config \ src/options \ $(SRC_LIBRARIES) \ - $(SRC_DYN_DEPENDENCIES) \ $(SRC_PROJECT_INITIALIZER) \ $(SRC_ANALYSES) \ $(SRC_CODE_GENERATOR) \ @@ -138,46 +131,6 @@ $(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 # ############### @@ -410,7 +363,6 @@ EACSL_SHARE_FILES = \ $(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES))) EACSL_DISTRIB_EXTERNAL =\ - $(EACSL_DISTRIB_DYNDEP) \ $(EACSL_SHARE_FILES) \ $(EACSL_MISC_FILES) \ $(EACSL_DOC_FILES) \ diff --git a/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml b/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml deleted file mode 100644 index 574d25ed1ab..00000000000 --- a/src/plugins/e-acsl/src/dependencies/dep_eva.disabled.ml +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 deleted file mode 100644 index a1af5ca1cb0..00000000000 --- a/src/plugins/e-acsl/src/dependencies/dep_eva.enabled.ml +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 deleted file mode 100644 index a151c251eeb..00000000000 --- a/src/plugins/e-acsl/src/dependencies/dep_eva.mli +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* *) -(* 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