diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index ebf83c405e98bd54ad5843e0e78a56e575028ea2..d1281c9707b84bdee3d01d511ba3835e809ec87c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -46,6 +46,7 @@ PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime
 PLUGIN_NO_DEFAULT_TEST:=yes
 
 tests/test_config: tests/test_config.in Makefile
+	$(PRINT_MAKING) $@
 	$(SED) -e "s|${FRAMAC_SHARE}|$(FRAMAC_SHARE)|g" \
 	       -e "s|@SEDCMD@|`which sed `|g" $< > $@
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
new file mode 100644
index 0000000000000000000000000000000000000000..8198e9065e16169091f2f3c9374da8b9e88dbd96
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
@@ -0,0 +1,3 @@
+/* run.config
+   COMMENT: testing the empty file
+   OPT: -e-acsl-project p -then-on p -print */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..91bc002d92cce8aa0b323cba7c71203a8446ce43
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle
@@ -0,0 +1,2 @@
+gcc: autom4te.cache/: linker input file unused because linking not done
+gcc: tests/: linker input file unused because linking not done
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..55ef4cfafc6b1a29447c1ffe20edd99ab7b98f1b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -0,0 +1,4 @@
+[kernel] preprocessing with "gcc -C -E -I.  autom4te.cache/"
+[kernel] preprocessing with "gcc -C -E -I.  tests/"
+/* Generated by Frama-C */
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle
index b999ffa90759e88ab50a596c422ba92b1e11dcd8..22d1d003cc7d5d759cc6b6acce13c4f18d4a5344 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle
@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-/tmp/frama_c_project_p3cd271i:15:[value] Assertion got status valid.
+PROJECT_FILE:15:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [dominators] computing for function main
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index e0309752413ccf7d3b4bc07ded592b243b9e33f6..eecef637f23b87ed7bf9143eea66a5a0b1c42c09 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,2 +1,2 @@
 CMD: @frama-c@ -cpp-command="gcc -C -E -I. -I${FRAMAC_SHARE}"
-FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"
+FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|[a-zA-Z/\\]\+frama_c_project_[a-z0-9]*|PROJECT_FILE|"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c9a8088700f9448b51bc18a41c606f8b86dd868f..4bf69d84dd570b56ddcbc11f35a12bc9c18953c0 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -30,11 +30,11 @@ let error s = raise (Typing_error s)
 let not_yet s =
   Options.not_yet_implemented "construct `%s' is not yet supported" s
 
-let e_acsl_fail () =
+let e_acsl_header () =
  GText("/*@ terminates \\false;\n\
 assigns \\nothing;\n\
 ensures \\false; */\n\
-void exit(int status);\n\
+extern void exit(int status);\n\
 \n\
 /*@ assigns \\nothing; */ \n\
 extern void eprintf(char * ); \n\
@@ -95,18 +95,19 @@ let convert_rooted acc generate (User a | AI(_, a)) =
 let convert_before_after acc generate (Before r | After r) =
   convert_rooted acc generate r
 
+let first_global = ref true
+
 class e_acsl_visitor prj generate = object
 
   inherit Visitor.generic_frama_c_visitor
     prj
     ((if generate then Cil.copy_visit else Cil.inplace_visit) ())
 
-  val mutable first_global = true
-
   method vglob g =
-    if first_global then
-      ChangeDoChildrenPost([ g ], fun l -> e_acsl_fail () :: l)
-    else
+    if !first_global then begin
+      first_global := false;
+      ChangeDoChildrenPost([ g ], fun l -> e_acsl_header () :: l)
+    end else
       DoChildren
 
   method vstmt_aux stmt =
@@ -125,7 +126,9 @@ class e_acsl_visitor prj generate = object
 end
 
 let do_visit ?(prj=Project.current ()) generate =
-  new e_acsl_visitor prj generate
+  let prj = new e_acsl_visitor prj generate in
+  first_global := true;
+  prj
 
 (*
 Local Variables: