From e59f37f992713c49f34f1a141037524493928fc7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 12 Sep 2013 08:02:31 +0000
Subject: [PATCH] [E-ACSL] hopefully lsl-cloud will be happy
---
src/plugins/e-acsl/Makefile.in | 9 +--------
src/plugins/e-acsl/pre_visit.ml | 4 +++-
src/plugins/e-acsl/tests/test_config.in | 2 +-
3 files changed, 5 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 2197a054725..516e1e79426 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -220,17 +220,10 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
ifeq (@MAY_RUN_TESTS@,yes)
-ifeq ($(FRAMAC_INTERNAL),yes)
-E_ACSL_SHARE=-e-acsl-share ./share/e-acsl
-else
-E_ACSL_SHARE=
-endif
-
$(E_ACSL_DIR)/tests/test_config: $(E_ACSL_DIR)/tests/test_config.in \
$(E_ACSL_DIR)/Makefile
$(PRINT_MAKING) $@
- $(SED) -e "s|@SHARE@|$(E_ACSL_SHARE)|g" \
- -e "s|@SEDCMD@|`which sed `|g" $< > $@
+ $(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
endif
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index 51c7636b161..de1503e78bc 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -292,7 +292,9 @@ class dup_functions_visitor prj = object (self)
->
self#next ();
let name = "__e_acsl_" ^ vi.vname in
- let new_vi = Project.on prj (Cil.makeGlobalVar name) vi.vtype in
+ let new_vi =
+ Project.on prj (Cil.makeGlobalVar ~generated:true name) vi.vtype
+ in
Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
Cil.DoChildrenPost
(fun l -> match l with
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index 2cf6f3c6767..d8e3a9da3ef 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,4 +1,4 @@
-CMD: @frama-c@ @SHARE@
+CMD: @frama-c@ -e-acsl-share ./share/e-acsl
OPT: -e-acsl-check -e-acsl-verbose 0
FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|`readlink -f $FRAMAC_SHARE`|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
COMMENT: The last regex works around the tendency of Frama-C to transform
--
GitLab