diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index eb3472ecd74ebbc3e080aca963a45add033a0e97..adbef2951fc0ef51349623fbac209b6a60e5f8eb 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -399,18 +399,25 @@ include $(FRAMAC_SHARE)/Makefile.dynamic EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES))) +EACSL_INSTALL_C_DIRECTORIES := \ + e-acsl \ + e-acsl/internals \ + e-acsl/instrumentation_model \ + e-acsl/observation_model \ + e-acsl/observation_model/internals \ + e-acsl/observation_model/bittree_model \ + e-acsl/observation_model/segment_model \ + e-acsl/numerical_model \ + e-acsl/libc_replacements + install:: $(PRINT_INSTALL) E-ACSL share files - $(MKDIR) $(FRAMAC_DATADIR)/e-acsl - $(CP) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl - $(MKDIR) $(FRAMAC_DATADIR)/e-acsl/bittree_model \ - $(FRAMAC_DATADIR)/e-acsl/segment_model - $(CP) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \ - $(FRAMAC_DATADIR)/e-acsl/bittree_model - $(CP) $(E_ACSL_DIR)/share/e-acsl/segment_model/* \ - $(FRAMAC_DATADIR)/e-acsl/segment_model - # manuals are not present in standard distribution. - # Don't fail because of that. + for dir in $(EACSL_C_DIRECTORIES); do \ + $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \ + $(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \ + done + # manuals are not present in standard distribution. + # Don't fail because of that. ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","") $(PRINT_INSTALL) E-ACSL manuals $(MKDIR) $(FRAMAC_DATADIR)/manuals diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml index 38f3fb5809f3adc1a37e721dbb726d3a46f31393..ee6ea93f43a2d2d564c12a518635989b55b589e3 100644 --- a/src/plugins/e-acsl/src/project_initializer/rtl.ml +++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml @@ -23,11 +23,7 @@ open Cil_types open Cil_datatype -let rtl_files () = - List.map - (fun d -> Options.Share.get_file ~mode:`Must_exist d) - [ "e_acsl_gmp_api.h"; - "e_acsl.h" ] +let rtl_file () = Options.Share.get_file ~mode:`Must_exist "e_acsl.h" (* create the RTL AST in a fresh project *) let create_rtl_ast prj = @@ -40,7 +36,7 @@ let create_rtl_ast prj = Kernel.Keep_unused_specified_functions.off (); Kernel.CppExtraArgs.add (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ())); - Kernel.Files.set (rtl_files ()); + Kernel.Files.set [ rtl_file () ]; Ast.get ()) ()