diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 2197a054725e2dd53cf7514f4561fdb6ac8624d3..516e1e79426e7f6e647f68f23187945a89dfdb5e 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 51c7636b1615ecf5c7bf9aad9f45b280e01c3503..de1503e78bc6f1b18bec888586a12e4b0a02f19d 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 2cf6f3c676728d6892fb674811660469ed5bc04d..d8e3a9da3ef9d6617d7d4cc01e4611f0e363de67 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