Skip to content
Snippets Groups Projects
Commit a3a64c43 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Update E-ACSL to use the new organisation of RTL files

parent 05be80b9
No related branches found
No related tags found
No related merge requests found
...@@ -399,18 +399,25 @@ include $(FRAMAC_SHARE)/Makefile.dynamic ...@@ -399,18 +399,25 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES))) 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:: install::
$(PRINT_INSTALL) E-ACSL share files $(PRINT_INSTALL) E-ACSL share files
$(MKDIR) $(FRAMAC_DATADIR)/e-acsl for dir in $(EACSL_C_DIRECTORIES); do \
$(CP) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
$(MKDIR) $(FRAMAC_DATADIR)/e-acsl/bittree_model \ $(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
$(FRAMAC_DATADIR)/e-acsl/segment_model done
$(CP) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \ # manuals are not present in standard distribution.
$(FRAMAC_DATADIR)/e-acsl/bittree_model # Don't fail because of that.
$(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.
ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","") ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","")
$(PRINT_INSTALL) E-ACSL manuals $(PRINT_INSTALL) E-ACSL manuals
$(MKDIR) $(FRAMAC_DATADIR)/manuals $(MKDIR) $(FRAMAC_DATADIR)/manuals
......
...@@ -23,11 +23,7 @@ ...@@ -23,11 +23,7 @@
open Cil_types open Cil_types
open Cil_datatype open Cil_datatype
let rtl_files () = let rtl_file () = Options.Share.get_file ~mode:`Must_exist "e_acsl.h"
List.map
(fun d -> Options.Share.get_file ~mode:`Must_exist d)
[ "e_acsl_gmp_api.h";
"e_acsl.h" ]
(* create the RTL AST in a fresh project *) (* create the RTL AST in a fresh project *)
let create_rtl_ast prj = let create_rtl_ast prj =
...@@ -40,7 +36,7 @@ let create_rtl_ast prj = ...@@ -40,7 +36,7 @@ let create_rtl_ast prj =
Kernel.Keep_unused_specified_functions.off (); Kernel.Keep_unused_specified_functions.off ();
Kernel.CppExtraArgs.add Kernel.CppExtraArgs.add
(Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ())); (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
Kernel.Files.set (rtl_files ()); Kernel.Files.set [ rtl_file () ];
Ast.get ()) Ast.get ())
() ()
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment