diff --git a/Makefile b/Makefile
index ac36580696193c88ba8341a49485e813c2a03299..4e51302ae7d5a8e69f5be2e9893ded7c39611b6e 100644
--- a/Makefile
+++ b/Makefile
@@ -958,6 +958,11 @@ PLUGIN_CMO:= options generator rte visit register
 PLUGIN_DISTRIBUTED:=yes
 PLUGIN_INTERNAL_TEST:=yes
 PLUGIN_TESTS_DIRS:=rte rte_manual
+PLUGIN_TESTS_LIB:=\
+  tests/rte/my_annotation/my_annotation.ml \
+  tests/rte/rte_api/rte_get_annot.ml \
+  tests/rte/compute_annot/compute_annot.ml \
+  tests/rte/my_annot_proxy/my_annot_proxy.ml
 $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
 
 #################
@@ -1406,17 +1411,18 @@ acsl_tests: byte
 	$(PRINT_EXEC) acsl_tests
 	find doc/speclang -name \*.c -exec ./bin/toplevel.byte$(EXE) {} \; > /dev/null
 
-LONELY_TESTS_ML_FILES=$(wildcard $(TEST_DIRS_AS_PLUGIN:%=tests/%/*.ml))
-LONELY_TESTS_BYTE_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmo)
-LONELY_TESTS_OPT_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmx)
-LONELY_TESTS_DYN_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmxs)
-$(LONELY_TESTS_BYTE_FILES): BFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-$(LONELY_TESTS_OPT_FILES): OFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-$(LONELY_TESTS_DYN_FILES): OFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-.PRECIOUS: $(LONELY_TESTS_OPT_FILES) \
-           $(LONELY_TESTS_DYN_FILES) \
-           $(LONELY_TESTS_BYTE_FILES) \
-           $(LONELY_TESTS_BYTE_FILES:%.cmo=%.cmi)
+LONELY_TESTS_ML_FILES:=\
+  $(shell find $(TEST_DIRS_AS_PLUGIN:%=tests/%) -name '*.ml')
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+  $(eval $(file:%.ml=%.cmo): BFLAGS+=-I $(dir $(file))))
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+  $(eval $(file:%.ml=%.cmx): OFLAGS+=-I $(dir $(file))))
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+  $(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file))))
+.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \
+           $(LONELY_TESTS_DYN_FILES:%.ml=%.cmxs) \
+           $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmo) \
+           $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmi)
 
 bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml
 	$(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $<
diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index 5478d009fa7e206bca7df4310e9062b357370d6a..423244b822a3af9883971dd6deabac001cfed778 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -80,7 +80,7 @@ PLUGIN_NO_DEFAULT_TEST:=yes
 endif
 
 PLUGIN_TESTS_DIRS:=aorai
-PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/aorai/Aorai_test.ml
+PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/aorai/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai/name_projects.ml
 
 include $(FRAMAC_SHARE)/Makefile.dynamic
 
@@ -101,7 +101,7 @@ $(Aorai_DIR)/tests/test_config_prove: \
 	$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
 	$(CHMOD_RO) $@
 
-Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/aorai/Aorai_test.cmxs $(Aorai_DIR)/tests/aorai/Aorai_test.cmo
+Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/aorai/Aorai_test.cmxs $(Aorai_DIR)/tests/aorai/Aorai_test.cmo $(Aorai_DIR)/tests/aorai/name_projects.cmxs $(Aorai_DIR)/tests/aorai/name_projects.cmo
 
 # Regenerating the Makefile on need
 
diff --git a/src/plugins/aorai/tests/aorai/assigns.c b/src/plugins/aorai/tests/aorai/assigns.c
index 7eb67e2087bbaa0ad8c729ab2efbf1bff2d8b1e9..c8d63fdb9dba75b9fb13a0021f32cf20f1435241 100644
--- a/src/plugins/aorai/tests/aorai/assigns.c
+++ b/src/plugins/aorai/tests/aorai/assigns.c
@@ -1,7 +1,8 @@
 /* run.config*
+   EXECNOW: make -s @PTEST_DIR@/name_projects.cmxs
    OPT: -aorai-automata tests/aorai/assigns.ya  -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
    OPT: -aorai-automata tests/aorai/assigns_det.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-   OPT: -aorai-automata tests/aorai/assigns.ya -load-script tests/aorai/name_projects.ml -aorai-test 1 -then -print
+   OPT: -aorai-automata tests/aorai/assigns.ya -load-module @PTEST_DIR@/name_projects -aorai-test 1 -then -print
 */
 
 int X;
diff --git a/src/plugins/wp/tests/wp_plugin/combined.c b/src/plugins/wp/tests/wp_plugin/combined.c
index e698ae498d812c5788580c80ab143b62567331da..33a5d1e193a283f4649865cca1511645456121ac 100644
--- a/src/plugins/wp/tests/wp_plugin/combined.c
+++ b/src/plugins/wp/tests/wp_plugin/combined.c
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-par 1 -load-script tests/wp_plugin/combined.ml
+   EXECNOW: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -wp-par 1 -load-module @PTEST_DIR@/@PTEST_NAME@
 */
 
 /* ZD : this should not be here such as it cannot be tested by all frama-c
diff --git a/src/plugins/wp/tests/wp_plugin/combined.ml b/src/plugins/wp/tests/wp_plugin/combined.ml
deleted file mode 100644
index 6b9da9a310774ff2577df057db2234f367d9d1b2..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/combined.ml
+++ /dev/null
@@ -1,22 +0,0 @@
-let main () =
-  Ast.compute ();
-  let module OLS = Datatype.List(Datatype.String) in
-  let module OKF = Datatype.Option(Kernel_function) in
-  let module OP = Datatype.Option(Property) in
-  Dynamic.get
-    ~plugin:"Wp" "wp_compute"
-    (Datatype.func3 OKF.ty OLS.ty OP.ty Datatype.unit)
-    (Some
-       (try Globals.Functions.find_by_name "job"
-        with Not_found -> assert false))
-    []
-    None;
-  let report =
-    Dynamic.get
-      ~plugin:"Report" "print" (Datatype.func Datatype.unit Datatype.unit)
-  in
-  report ();
-  !Db.Value.compute ();
-  report ()
-
-let () = Db.Main.extend main
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 299e5c4b1a5a9d3ef52579e0104f2e788c80b53b..c8a980291364c79ed27ab5f1a70676174e4b91f0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -7,7 +7,7 @@
   Function job
 ------------------------------------------------------------
 
-Goal Assertion (file tests/wp_plugin/combined.c, line 26):
+Goal Assertion (file tests/wp_plugin/combined.c, line 27):
 Assume {
   Type: is_sint32(A).
   (* Heap *)
@@ -17,7 +17,7 @@ Prove: (50 <= A) /\ (A <= 100).
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 28):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 29):
 Assume {
   Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
   (* Heap *)
@@ -39,12 +39,12 @@ Prove: (-1) <= i.
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 28):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 29):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 29):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 30):
 Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50).
 Assume {
   Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
@@ -68,12 +68,12 @@ Prove: P_P(a[shift_sint32(t, i) <- v][shift_sint32(t, i_1)]).
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 29):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 30):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 34):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 35):
 Let x = 1 + j.
 Assume {
   Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j) /\ is_sint32(x).
@@ -98,12 +98,12 @@ Prove: A <= x.
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 34):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 35):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion (file tests/wp_plugin/combined.c, line 39):
+Goal Assertion (file tests/wp_plugin/combined.c, line 40):
 Let a = havoc(Mint_undef_1, Mint_0, shift_sint32(t, 0), 50).
 Assume {
   Type: is_sint32(A) /\ is_sint32(i_1) /\ is_sint32(j).
@@ -130,36 +130,36 @@ Prove: P_P(havoc(Mint_undef_0, a, shift_sint32(t, A), 100 - A)
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (1/3):
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (2/3):
-Effect at line 32
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (2/3):
+Effect at line 33
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (3/3):
-Call Result at line 32
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (3/3):
+Call Result at line 33
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (1/3):
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (2/3):
-Effect at line 37
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (2/3):
+Effect at line 38
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (3/3):
-Call Result at line 37
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (3/3):
+Call Result at line 38
 Let a = shift_sint32(t, j).
 Assume {
   Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j).
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index ccf98764fd086b47e1a139aa5743a4fee0a9b313..d6e1f53181467a2ec7876261086d4a39869f7d19 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,6 +1,7 @@
 /* run.config*
+EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
 OPT: -eva-show-progress -print -journal-disable -eva -report
-OPT: -load-script tests/builtins/big_local_array_script.ml -then-on prj -print -report
+OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
 OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva
 */
 
diff --git a/tests/float/fval_test.i b/tests/float/fval_test.i
index 26ba3db86ad924f7b9f40abffef09d28f84b893a..cabb28768924493f9964d6329934d0356b2e5143 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,6 +1,6 @@
 /* run.config
-#   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
 */
 /* run.config*
    DONTRUN:
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 03c9193098e1b927237577588f973faaeb7a6e45..8a7acc8e682ff542811632ac5f9436e3a9a0f4f9 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -5,10 +5,10 @@
   OPT: -load-script tests/journal/result/control_journal -journal-disable
   CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
   OPT: -load-script tests/journal/result/control_journal_bis -calldeps -journal-disable
-  EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script tests/journal/abstract_cpt.ml -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null
+  EXECNOW: make -s @PTEST_DIR@/abstract_cpt.cmxs
+  EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null
   CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
-  OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-script tests/journal/abstract_cpt.ml -load-script tests/journal/use_cpt.ml
-  
+  OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml
 */
 
 int x,y,c,d;
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 5b85156aea37ea5d264a52c07910e37b9eb1d4cd..a153d1c9351f7ef7834f70249424f329c70eaeb7 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -1,7 +1,10 @@
 /* run.config*
-   OPT: -load-script tests/libc/check_libc_naming_conventions.ml -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-script tests/libc/check_const.ml -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
+   EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs
+   EXECNOW: make -s @PTEST_DIR@/check_const.cmxs
+   EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs
+   OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
    OPT: -print -print-libc
-   OPT: -load-script tests/libc/check_parsing_individual_headers.ml
+   OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers.ml
    CMD: ./tests/libc/check_full_libc.sh
    OPT:
 **/
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index ffa163ed517ced7ae131d1bd9f87f61300909256..c1ea9b1264b8f540555594d7684ce6cc084d13d7 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/libc/fc_libc.c:157: assertion got status valid.
-[eva] tests/libc/fc_libc.c:158: assertion got status valid.
-[eva] tests/libc/fc_libc.c:159: assertion got status valid.
 [eva] tests/libc/fc_libc.c:160: assertion got status valid.
+[eva] tests/libc/fc_libc.c:161: assertion got status valid.
+[eva] tests/libc/fc_libc.c:162: assertion got status valid.
+[eva] tests/libc/fc_libc.c:163: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index e92b67f2a8e902f76929347cdee85a7b35688149..f7a377dc16250f21911dbc5f014d7a50b33bac3f 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -1,5 +1,6 @@
 /* run.config*
-OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-script @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.ml -machdep custom -print -then -print
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.cmxs
+OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-module @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@ -machdep custom -print -then -print
 COMMENT: we need a -then to test double registering of a machdep
 */
 
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index 33f9b14b6af9429fe2f06314e5b217562ab33b52..e5c6f3a5f23f1f5e9fbe1a0f713c81101ead221d 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
 */
 
 int* f() {
diff --git a/tests/misc/oracle/log_twice.res.oracle b/tests/misc/oracle/log_twice.res.oracle
index 871920c55ba2fee41bfc176a78c22e59d809ea86..30fcb6869ca0f742ade2702953dcb5493a9573e9 100644
--- a/tests/misc/oracle/log_twice.res.oracle
+++ b/tests/misc/oracle/log_twice.res.oracle
@@ -5,19 +5,19 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function f <- main.
-  Called from tests/misc/log_twice.i:11.
+  Called from tests/misc/log_twice.i:12.
 [eva] Recording results for f
 [eva] Done for function f
-[eva:locals-escaping] tests/misc/log_twice.i:11: Warning: 
+[eva:locals-escaping] tests/misc/log_twice.i:12: Warning: 
   locals {x} escaping the scope of f through \result<f>
-[eva:alarm] tests/misc/log_twice.i:12: Warning: 
+[eva:alarm] tests/misc/log_twice.i:13: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
-[kernel] tests/misc/log_twice.i:12: Warning: 
+[kernel] tests/misc/log_twice.i:13: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
 [eva] Recording results for main
 [eva] done for function main
-[eva] tests/misc/log_twice.i:12: 
+[eva] tests/misc/log_twice.i:13: 
   assertion 'Eva,dangling_pointer' got final status invalid.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -25,17 +25,17 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function f <- main.
-  Called from tests/misc/log_twice.i:11.
+  Called from tests/misc/log_twice.i:12.
 [eva] Recording results for f
 [eva] Done for function f
-[eva:locals-escaping] tests/misc/log_twice.i:11: Warning: 
+[eva:locals-escaping] tests/misc/log_twice.i:12: Warning: 
   locals {x} escaping the scope of f through \result<f>
-[eva:alarm] tests/misc/log_twice.i:12: Warning: 
+[eva:alarm] tests/misc/log_twice.i:13: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
-[kernel] tests/misc/log_twice.i:12: Warning: 
+[kernel] tests/misc/log_twice.i:13: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
 [eva] Recording results for main
 [eva] done for function main
-[eva] tests/misc/log_twice.i:12: 
+[eva] tests/misc/log_twice.i:13: 
   assertion 'Eva,dangling_pointer' got final status invalid.
diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i
index 3fc9e30144b24c39aacd54b9183f1f5617cb66e7..a03c0cd1c45050418effd185243b6dff7a1f7e3e 100644
--- a/tests/misc/visitor_creates_func_bts_1349.i
+++ b/tests/misc/visitor_creates_func_bts_1349.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -load-script tests/misc/Visitor_creates_func_bts_1349.ml -then-on test -print
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -then-on test -print
 */
 
 int a = 10;
diff --git a/tests/misc/Visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
similarity index 100%
rename from tests/misc/Visitor_creates_func_bts_1349.ml
rename to tests/misc/visitor_creates_func_bts_1349.ml
diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c
index c0fa077572c7ecee3e969ee0e4d7eee56031aec2..3efc61ce72bd3318339f327989bcf123587acb84 100644
--- a/tests/pdg/sets.c
+++ b/tests/pdg/sets.c
@@ -1,6 +1,6 @@
 /* run.config
-#   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -eva-show-progress -load-script @PTEST_DIR@/@PTEST_NAME@.ml -lib-entry -main f -pdg -inout -journal-disable  -pdg-print -pdg-verbose 2
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -eva-show-progress -load-module @PTEST_DIR@/@PTEST_NAME@ -lib-entry -main f -pdg -inout -journal-disable  -pdg-print -pdg-verbose 2
 */
 
 
diff --git a/tests/rte/precond2.c b/tests/rte/precond2.c
index 2c3844e757435034d26935ecf9cfd2dcc952e029..72d360e0d96667335f976b60727fdeb9843b965c 100644
--- a/tests/rte/precond2.c
+++ b/tests/rte/precond2.c
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -warn-special-float none -load-script tests/rte/compute_annot/compute_annot.ml -journal-disable
+   EXECNOW: make -s @PTEST_DIR@/compute_annot/compute_annot.cmxs
+   OPT: -warn-special-float none -load-module @PTEST_DIR@/compute_annot/compute_annot -journal-disable
 */
 
 int global = 15;
diff --git a/tests/rte/threefunc.c b/tests/rte/threefunc.c
index 44aa8d37cd24c7e8fbd3027e21a2ead6d43c24d6..6220079b7feaa8713e5d861840c7887d26a65abb 100644
--- a/tests/rte/threefunc.c
+++ b/tests/rte/threefunc.c
@@ -1,5 +1,6 @@
 /* run.config
-OPT: -load-script tests/rte/my_annotation/my_annotation.ml
+EXECNOW: make -s @PTEST_DIR@/my_annotation/my_annotation.cmxs
+OPT: -load-module @PTEST_DIR@/my_annotation/my_annotation.ml
 */
 
 
diff --git a/tests/rte/twofunc.c b/tests/rte/twofunc.c
index 38ce35dac65ffdac7071447de3145e63aa84bed7..2732ad9f1f99b79c79b2f9450870d3904a69cd71 100644
--- a/tests/rte/twofunc.c
+++ b/tests/rte/twofunc.c
@@ -1,5 +1,6 @@
 /* run.config
-OPT: -load-script tests/rte/my_annot_proxy/my_annot_proxy.ml
+EXECNOW: make -s @PTEST_DIR@/my_annot_proxy/my_annot_proxy.cmxs
+OPT: -load-module @PTEST_DIR@/my_annot_proxy/my_annot_proxy
 */
 
 
diff --git a/tests/rte/twofunc3.c b/tests/rte/twofunc3.c
index 8894e7cbee4a51fb176dc870a4302db5171ae2ad..b7102aaf7086db45e0bfbf0924a346a8edab1bcb 100644
--- a/tests/rte/twofunc3.c
+++ b/tests/rte/twofunc3.c
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -load-script tests/rte/rte_api/rte_get_annot.ml -journal-disable
+   EXECNOW: make -s @PTEST_DIR@/rte_api/rte_get_annot.cmxs
+   OPT: -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
 */
 
 
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index 0a37b04868e6eb4a445e152669dc49e7ee6ba869..e0d5d8f8b74aa58031d88339800120da3fb0c659 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -6,8 +6,9 @@
    CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable -print
    OPT: -load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable
-   EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-script tests/saveload/status.ml -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
-   OPT: -load-script tests/saveload/status.ml -load ./tests/saveload/result/status.sav
+   EXECNOW: make -s @PTEST_DIR@/status.cmxs
+   EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
+   OPT: -load-module @PTEST_DIR@/status -load ./tests/saveload/result/status.sav
    OPT: -load ./tests/saveload/result/status.sav
 */
 
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index 985eb96467566d2d7978358d57e350538de45307..056059606204259f47c4619d6aa71f6dd14adaa0 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -4,9 +4,9 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/saveload/basic.i:18: assertion got status valid.
-[eva] tests/saveload/basic.i:19: starting to merge loop iterations
-[eva:alarm] tests/saveload/basic.i:19: Warning: 
+[eva] tests/saveload/basic.i:19: assertion got status valid.
+[eva] tests/saveload/basic.i:20: starting to merge loop iterations
+[eva:alarm] tests/saveload/basic.i:20: Warning: 
   signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index 985eb96467566d2d7978358d57e350538de45307..056059606204259f47c4619d6aa71f6dd14adaa0 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -4,9 +4,9 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/saveload/basic.i:18: assertion got status valid.
-[eva] tests/saveload/basic.i:19: starting to merge loop iterations
-[eva:alarm] tests/saveload/basic.i:19: Warning: 
+[eva] tests/saveload/basic.i:19: assertion got status valid.
+[eva] tests/saveload/basic.i:20: starting to merge loop iterations
+[eva:alarm] tests/saveload/basic.i:20: Warning: 
   signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index 746e8d2af98b3db40957b366930d9684aa572716..884e57b2162c1665bbac00b98c150d5e02c6373c 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,6 +1,6 @@
 /* run.config
 #   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml -eva -eva-show-progress -journal-disable
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva -eva-show-progress -journal-disable
 */
 
 
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index ec1994bfe925546eb0abd2a6e017c834b22b6bff..c94e20665e6bda514c2d2f3460c2c132504d509c 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -print -load-script ./@PTEST_DIR@/@PTEST_NAME@.ml
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@
 */
 
 /*@ behavior foo: ensures \true; */
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index f87954814a8e3d056d969c21a0df2de678014fe9..a3fbe427e1e26c1733ff8eecd4e4bd29fa9270d3 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,5 +1,6 @@
-/* run.config 
-   OPT:-print -load-script tests/syntax/machdep_char_unsigned.ml -machdep unsigned_char -then -constfold -rte
+/* run.config
+   EXECNOW: make -s @PTEST_DIR@/machdep_char_unsigned.cmxs
+   OPT:-print -load-module @PTEST_DIR@/machdep_char_unsigned -machdep unsigned_char -then -constfold -rte
 */
 char t[10];
 
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index bd5fafc82529eaebcf8b59565b318814197820d4..a20b81af83fc0cb5b769207afd287f77450a2a17 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,7 +1,8 @@
 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@_bis.cmxs
 OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-script @PTEST_DIR@/@PTEST_NAME@_bis.ml -test -then-on filtered -print
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@_bis -test -then-on filtered -print
 */
 
 #include "stdio.h"
diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i
index 6d8082506687116f05472ed8e711b5cee580024e..9570e109382c07d8d19a57248a384cbc372b9e66 100644
--- a/tests/syntax/logic_env.i
+++ b/tests/syntax/logic_env.i
@@ -1,5 +1,6 @@
 /* run.config
-OPT: -load-script tests/syntax/logic_env_script.ml
+EXECNOW: make -s @PTEST_DIR@/logic_env_script.cmxs
+OPT: -load-module @PTEST_DIR@/logic_env_script
 */
 
 //@ predicate foo(integer x) = x == 0;
diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c
index fac8ea328939009b61a97e51f0f01a2d5e03c945..33a8d6c3537a3452d299e6a481c5514bbdb93022 100644
--- a/tests/syntax/typedef_multi_1.c
+++ b/tests/syntax/typedef_multi_1.c
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -load-script tests/syntax/typedef_multi.ml tests/syntax/typedef_multi_2.c
+   EXECNOW: make -s @PTEST_DIR@/typedef_multi.cmxs
+   OPT: -load-module @PTEST_DIR@/typedef_multi tests/syntax/typedef_multi_2.c
 */
 
 #include "tests/syntax/typedef_multi.h"