more robust tests

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" $< > $@
 

src/plugins/e-acsl/tests/e-acsl-runtime/empty.i

+/* run.config
+   COMMENT: testing the empty file
+   OPT: -e-acsl-project p -then-on p -print */

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle

+gcc: autom4te.cache/: linker input file unused because linking not done
+gcc: tests/: linker input file unused because linking not done

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle

+[kernel] preprocessing with "gcc -C -E -I.  autom4te.cache/"
+[kernel] preprocessing with "gcc -C -E -I.  tests/"
+/* Generated by Frama-C */
+

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

src/plugins/e-acsl/tests/test_config.in

 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|"

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: