diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c
index c760aa1537ec7d120bb213e1eeab4c0df7da9ef0..0e1c52123e21895c27435d990845fc0d5bfb3cf1 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,7 +1,7 @@
 /* run.config*
    OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
    OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-   MODULE: @PTEST_DIR@/name_projects.cmxs
+ MODULE: name_projects
    OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
 */
 
diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
index 5b30c58d98030efe6ba865ee764fc5e8b7140d86..d47e55b06a7c8c2cdf82956684ed5053371d2249 100644
--- a/tests/cil/insert_formal.i
+++ b/tests/cil/insert_formal.i
@@ -1,5 +1,5 @@
 /* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 OPT: -print
 */
 
diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i
index ebf24f803a0115aca137855c9a076f888475e119..4bb64bd9e320da49d389c5ca31c26dd7393d6d9a 100644
--- a/tests/cil/mkBinOp.i
+++ b/tests/cil/mkBinOp.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -machdep x86_32 -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold
+MODULE: @PTEST_NAME@
+OPT: -machdep x86_32 -no-autoload-plugins -print -constfold
 */
 
 int main(void) {
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c
index 959842971acaa01ca6b96c2891898086bd098d45..a9778533534d5e510cdeea361db9ffe7682b488b 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.c
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -deps -journal-disable
+   MODULE: @PTEST_NAME@
+   OPT: -eva @EVA_OPTIONS@ -deps -journal-disable
 */
 
 int x,y,z;
diff --git a/tests/float/fval_test.i b/tests/float/fval_test.i
index f480093ba099eda06a2fdca943402b02945c5cce..7cb38611d3a0c2ae466b20e6ee7bf17f9b0836d9 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT:
 */
 /* run.config*
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index dea5fdbface5e49569a2d52996e69ac8b4d52f06..71676ee94fde86777dcac52dfb32ac462dbeba74 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,7 +1,7 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
-   CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
+   EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
+   CMD: @frama-c@
    OPT: -load-script tests/journal/result/intra_journal -journal-disable
 */
 
diff --git a/tests/misc/behavior_names.i b/tests/misc/behavior_names.i
index 20a66a894482270937c3af919cdc95bcc68f1a90..63b97f6a7a24ff5d8474c4be502adeaa29c97e11 100644
--- a/tests/misc/behavior_names.i
+++ b/tests/misc/behavior_names.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT: -no-autoload-plugins
 */
 
diff --git a/tests/misc/debug_category.i b/tests/misc/debug_category.i
index 6b4a7dbc2c393c816be2d930b7eb81d6d0deb33a..f4b77fa6c365afe2abb45fb1aa71d9299e60b189 100644
--- a/tests/misc/debug_category.i
+++ b/tests/misc/debug_category.i
@@ -1,5 +1,5 @@
 /* run.config*
-MODULE: tests/misc/Debug_category.cmxs
+MODULE: Debug_category
 EXIT: 0
   OPT: -test-msg-key help -test-warn-key="a=inactive"
   OPT: -test-msg-key a -test-warn-key="a=inactive"
diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i
index 40748281b882ec47152214f8f72222330294a30b..6ae8e0fd0e9b4d1322f35cd50ae3a3eceaf37cfd 100644
--- a/tests/misc/filepath.i
+++ b/tests/misc/filepath.i
@@ -1,6 +1,6 @@
 /* run.config*
-   MODULE: tests/misc/filepath_test.cmxs
-   COMMENT: the '-load' option below intentionally contains an error
+ MODULE: filepath_test
+ COMMENT: the '-load' option below intentionally contains an error
  EXIT: 1
    OPT: -no-autoload-plugins -load nonexistent_file.sav
  */
diff --git a/tests/misc/version.i b/tests/misc/version.i
index 2b739ebbd83e2b125fd1e0c738864c54c1df21c7..3691d73eeae5a30ce342087d0795aeec6260ca48 100644
--- a/tests/misc/version.i
+++ b/tests/misc/version.i
@@ -1,4 +1,4 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT: -no-autoload-plugins
 */
diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c
index 7b8f05dda8ace56c924d35a30447621d1971e2ff..400b9cdfb01723da987dcea735efe06dc95e5560 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
-   STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@ -lib-entry -main f -pdg -inout "
+ MODULE: @PTEST_NAME@
+   STDOPT: +"-lib-entry -main f -pdg -inout "
 */
 
 
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index b50076a1a38082a0c1f3d15ae9b1cfa66e8fa6e0..24716e1928853c5f80851385f3bd06a00519ae20 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -journal-disable -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -main main2
+   MODULE: @PTEST_NAME@
+   OPT: -journal-disable -then -main main2
 */
 /* bug 971: */
 volatile foo;
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index acafbd74299ae375c471c6e8fd9274ea62343f4a..e8808595b16aee5132fb1348e55883ea9f6552d1 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,5 +1,5 @@
 /* run.config
-#   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+#   MODULE: @PTEST_NAME@
    OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva @EVA_OPTIONS@ -journal-disable
 */
 
diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index 85228eb7dfdf70924f95f5c26350fd051eff3b58..05de1247ae25313960ec60e72811bcca175d6f35 100644
--- a/tests/spec/Extend.i
+++ b/tests/spec/Extend.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -copy -kernel-warn-key=annot-error=active
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -copy -kernel-warn-key=annot-error=active
 */
 
 /*@ foo x == 0;
diff --git a/tests/spec/Extend_preprocess.i b/tests/spec/Extend_preprocess.i
index 24b2d061048798182dd865eb746bead6b33d6fa9..cf9e4d135789e7e9bf81a8218f71b6dc598425b9 100644
--- a/tests/spec/Extend_preprocess.i
+++ b/tests/spec/Extend_preprocess.i
@@ -1,5 +1,5 @@
 /* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
 */
 
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index 319f9310fa3a995bdca92dff5499c6d5e940bd69..ea7924d97dbe9d93159668c275655b2bee3e9f99 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -1,5 +1,5 @@
 /* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
 */
 
diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i
index d3f776e538ad9fab7fb58da166532e67a394872e..97812f290c0423084d318ac9af637987e6b800be 100644
--- a/tests/spec/Extend_short_print.i
+++ b/tests/spec/Extend_short_print.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins
 */
 
 /*@
diff --git a/tests/spec/add_global.i b/tests/spec/add_global.i
index 7ed406648a9ae0f6d2d9f3d5357314714edf358c..08d58179a4b810bfd3400be37a49ef983baea968 100644
--- a/tests/spec/add_global.i
+++ b/tests/spec/add_global.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -print
 */
 
 int main () { return 0; }
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
index 87084d55a6f8bf65ebb9dee4f0a8bc91f733d85e..d921cdd4e849b73c77465cb88691dc8b70d366ff 100644
--- a/tests/spec/assigns_from_kf.i
+++ b/tests/spec/assigns_from_kf.i
@@ -1,5 +1,5 @@
 /* run.config
-  MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+  MODULE: @PTEST_NAME@
   OPT: -kernel-warn-key ghost:bad-use=inactive -print
 */
 // Note: we deactivate "ghost:bad-use" because the typing phase checks on call
diff --git a/tests/spec/boolean_conversion.i b/tests/spec/boolean_conversion.i
index 1c815309a3d59eae140fbaf562c456a41d43dc56..78edea3a0b7a3f9b8e788fc5c56c7151fbc6e644 100644
--- a/tests/spec/boolean_conversion.i
+++ b/tests/spec/boolean_conversion.i
@@ -1,5 +1,5 @@
 /* run.config*
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 STDOPT:
 */
 void __FC_assert(int c);
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index c94e20665e6bda514c2d2f3460c2c132504d509c..7cdc9f445b4ece5ee771342d9b115f5a08cddb8a 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@
+ MODULE: @PTEST_NAME@
+   OPT: -print -no-autoload-plugins
 */
 
 /*@ behavior foo: ensures \true; */
diff --git a/tests/spec/bts0655.i b/tests/spec/bts0655.i
index b5947620ab99b29f05efcec6781e7549d0ff63c8..160d6aa62b376d8be8b5e08d8423ecafa5fce29d 100644
--- a/tests/spec/bts0655.i
+++ b/tests/spec/bts0655.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 /*@
   @ ensures \result == \max( a, b );
diff --git a/tests/spec/comparison.i b/tests/spec/comparison.i
index a62a8a65c779ed28e8b1795d4182dc1a0897c66e..d29dcb424b11c7d884ed268d8086caba78cffc3e 100644
--- a/tests/spec/comparison.i
+++ b/tests/spec/comparison.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 /*@ predicate foo(boolean a, boolean b) = a == b; */
diff --git a/tests/spec/expr_to_term.i b/tests/spec/expr_to_term.i
index 88b15b296dc5a2eefe1be5362249a5181c778658..97a83ecea582933f3cb466683a69953bacd4734a 100644
--- a/tests/spec/expr_to_term.i
+++ b/tests/spec/expr_to_term.i
@@ -1,5 +1,5 @@
 /* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 OPT: -keep-logical-operators -print
 */
 
diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
index c3c61836044e2aa33369d00e439c5806eff9e106..a56330e2b6adbb6f458c94f51455f709483204a9 100644
--- a/tests/spec/extend_extern.i
+++ b/tests/spec/extend_extern.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT:
  */
 /*@ predicate load(char * x) = \true ; */
diff --git a/tests/spec/heterogeneous_set_bts1146.i b/tests/spec/heterogeneous_set_bts1146.i
index 98c508eb2fd3422ae25f8f98047f6ca9989216e9..bce7b3a7b2cf1e600725bc9c9836e464881916ca 100644
--- a/tests/spec/heterogeneous_set_bts1146.i
+++ b/tests/spec/heterogeneous_set_bts1146.i
@@ -1,7 +1,7 @@
 /* run.config
    DONTRUN: bugfix in progress
-   EXECNOW: make -s tests/spec/Type_of_term.cmxs
-   OPT: -load-module ./tests/spec/Type_of_term.cmxs -print
+ MODULE: Type_of_term
+   OPT: -no-autoload-plugins -print
 */
 
 /*@ lemma foo: \union(1) == \union(1.0); */
diff --git a/tests/spec/location_char.c b/tests/spec/location_char.c
index 99339a087cfd144ae6a400c10249fa9394530e4b..bdfc8dbeab1aa6c114997676739326f9172cb026 100644
--- a/tests/spec/location_char.c
+++ b/tests/spec/location_char.c
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins
 */
 
 /*@ requires x <= 0;
diff --git a/tests/spec/logic_functions_sets.i b/tests/spec/logic_functions_sets.i
index 60190e8cc24bd8a26fac50e8dd246aeb7f79e3c0..1ab710d70bf133f774a77f23f42e187ed71baf17 100644
--- a/tests/spec/logic_functions_sets.i
+++ b/tests/spec/logic_functions_sets.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT: -no-autoload-plugins
 */
 
diff --git a/tests/spec/loop_assigns_generated.i b/tests/spec/loop_assigns_generated.i
index f85c8c5a1ccec3e842a459fe4f1df20aee349285..0543d6904395a45fa0595de9c2cbeeaef0874739 100644
--- a/tests/spec/loop_assigns_generated.i
+++ b/tests/spec/loop_assigns_generated.i
@@ -1,5 +1,5 @@
 /* run.config*
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
 OPT:
 */
 
diff --git a/tests/spec/model.i b/tests/spec/model.i
index 840ab0193bc7883a50f8671c43f01ad4264e3c08..4faeec7d188d946640c28fdfc7fccdf538f3b258 100644
--- a/tests/spec/model.i
+++ b/tests/spec/model.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+MODULE: @PTEST_NAME@
+STDOPT: +"-no-autoload-plugins"
 */
 struct S { int x; int y; };
 typedef struct S T;
diff --git a/tests/spec/pp_empty_spec.i b/tests/spec/pp_empty_spec.i
index 6d337f8500a51c4c764145969e8ef1c73bcff1f0..7890ba4a2f0977956094d6784fb2af12bbed84ce 100644
--- a/tests/spec/pp_empty_spec.i
+++ b/tests/spec/pp_empty_spec.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
  */
 int main(void) {
     int x = 0;
diff --git a/tests/spec/property_test.i b/tests/spec/property_test.i
index 6f1de940f0cb8b128f6d9fefa4c635c806f5a267..a638952ac377e6f0e07e5ba1f5afc439ed59309e 100644
--- a/tests/spec/property_test.i
+++ b/tests/spec/property_test.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 int X;
diff --git a/tests/spec/status_by_call_issue_890.i b/tests/spec/status_by_call_issue_890.i
index d3209b6bea950aca95d9ac3a3ec582596fade641..7102449b8d3bc9df40d73f6cb4918508be9368de 100644
--- a/tests/spec/status_by_call_issue_890.i
+++ b/tests/spec/status_by_call_issue_890.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
 */
 
 struct list { struct list *next; };
diff --git a/tests/spec/type_constructors_in_env.i b/tests/spec/type_constructors_in_env.i
index 636049ed329cfd848d51760fd52d2d84701261fc..f7525f869c8582c3bc07805b494135a8e5c15bd6 100644
--- a/tests/spec/type_constructors_in_env.i
+++ b/tests/spec/type_constructors_in_env.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 /*@ type foo = A | B; */
diff --git a/tests/spec/type_of_term.i b/tests/spec/type_of_term.i
index 81964fc9dbe8b52e417a7aac83b5e34436a2d08d..b117a9ee9455c21c18e530c69450331dacc411fe 100644
--- a/tests/spec/type_of_term.i
+++ b/tests/spec/type_of_term.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/spec/Type_of_term.cmxs
-   OPT: -load-module tests/spec/Type_of_term.cmxs -print
+ MODULE: Type_of_term
+   STDOPT:
 */
 
 int t [42];
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index edf44c1c372287804691d41291d1cbd5f120a9b7..6bf2f55e42ef1cd1009a5f8de7b7962f3349a710 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @EVA_OPTIONS@
+ MODULE: @PTEST_NAME@
+   OPT: @EVA_OPTIONS@
 */
 
 struct S { int i; };
diff --git a/tests/syntax/add_allocates.i b/tests/syntax/add_allocates.i
index 2153e41ea67e6f54eeaf4a2b2719f3abb359eeac..67b339d8fed71a552311f26f17790ccb27de365e 100644
--- a/tests/syntax/add_allocates.i
+++ b/tests/syntax/add_allocates.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+ MODULE: @PTEST_NAME@
+   STDOPT:
 */
 
 
diff --git a/tests/syntax/ast_init.i b/tests/syntax/ast_init.i
index 1e9aad67b5d3289f2c50f423edf4697fb2fb77fa..7e0d7dd7df19c94d94437d236a486d60872ff336 100644
--- a/tests/syntax/ast_init.i
+++ b/tests/syntax/ast_init.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 int f(int x) { return x; }
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index a3fbe427e1e26c1733ff8eecd4e4bd29fa9270d3..771ea26e6800c6fac56c23f00561be16aeda4fce 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,6 +1,6 @@
 /* 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
+ MODULE: machdep_char_unsigned
+   OPT:-print -machdep unsigned_char -then -constfold -rte
 */
 char t[10];
 
diff --git a/tests/syntax/clone_test.i b/tests/syntax/clone_test.i
index 7d94b47b61384b15dac0b60062acd1148947726a..358db8f4602eac5212531f45910817cfcc9caf8d 100644
--- a/tests/syntax/clone_test.i
+++ b/tests/syntax/clone_test.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+  MODULE: @PTEST_NAME@
+    OPT: -no-autoload-plugins
 */
 
 /*@
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index a20b81af83fc0cb5b769207afd287f77450a2a17..ec7e1ab180571bc3edbdc5ddafa90c2a602d0b21 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,8 +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-module @PTEST_DIR@/@PTEST_NAME@_bis -test -then-on filtered -print
+ MODULE: @PTEST_NAME@
+   OPT:
+ MODULE: @PTEST_NAME@_bis
+   OPT: -test -then-on filtered -print
 */
 
 #include "stdio.h"
diff --git a/tests/syntax/enum_repr.i b/tests/syntax/enum_repr.i
index 8cf7d3d4b1fca5a3becbcb2dd97297ce76f22f92..bee2bcb681f7d1481bcc40aff50666a57240b910 100644
--- a/tests/syntax/enum_repr.i
+++ b/tests/syntax/enum_repr.i
@@ -1,8 +1,8 @@
 /* run.config
-EXECNOW: make -s tests/syntax/Enum_repr.cmxs
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums int -print
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-short-enums -print
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-enums -print
+ MODULE: Enum_repr
+   OPT: -machdep x86_32 -enums int -print
+   OPT: -machdep x86_32 -enums gcc-short-enums -print
+   OPT: -machdep x86_32 -enums gcc-enums -print
 */
 
 // is represented by | int | gcc-enums          | gcc-short-enums
diff --git a/tests/syntax/forloophook.i b/tests/syntax/forloophook.i
index d9e38bd7b222e52182a102421f32151e285020ec..918fadf7579d70cc8ad34bbc1f60f0007ea9d5ac 100644
--- a/tests/syntax/forloophook.i
+++ b/tests/syntax/forloophook.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 void f() {
   for (int i=0; i< 10; i++);
diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i
index 93a7dc265a729926ce94aac380f8ec67a67198b8..0b767a1328585f2b970022d3318315d8d381ec7d 100644
--- a/tests/syntax/formals_decl_leak.i
+++ b/tests/syntax/formals_decl_leak.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -print -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @PTEST_DIR@/@PTEST_NAME@_1.i
+ MODULE: @PTEST_NAME@
+   OPT: -print -no-autoload-plugins @PTEST_DIR@/@PTEST_NAME@_1.i
 */
 
 void f(int x);
diff --git a/tests/syntax/get_astinfo_bts1136.i b/tests/syntax/get_astinfo_bts1136.i
index 694aacdf37979df8db7e8043f9ed6268c82efa73..0e47cfb677f9326cc88e902cb59a389d92ec1fdc 100644
--- a/tests/syntax/get_astinfo_bts1136.i
+++ b/tests/syntax/get_astinfo_bts1136.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 int f (int x) { return x; }
 int g (int x) { return x; }
diff --git a/tests/syntax/ghost_parameters_formals_status.i b/tests/syntax/ghost_parameters_formals_status.i
index 4698b9f77e2e313d832db47fc4a41b83371508e5..b83bc5cd530c5b26ce1de792d903228d5821b270 100644
--- a/tests/syntax/ghost_parameters_formals_status.i
+++ b/tests/syntax/ghost_parameters_formals_status.i
@@ -1,6 +1,6 @@
 /* run.config
-  EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-  OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 void declaration_void(void) /*@ ghost (int x, int y) */ ;
diff --git a/tests/syntax/inserted_casts.c b/tests/syntax/inserted_casts.c
index 805496d3d23a36a8bb973199a0e95203a72363ab..bd24edbeace53b6a81106a9417ecd0ea474a0d32 100644
--- a/tests/syntax/inserted_casts.c
+++ b/tests/syntax/inserted_casts.c
@@ -1,7 +1,7 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
-   STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" +"-machdep x86_64"
+   MODULE: @PTEST_NAME@
+   STDOPT: +"-no-autoload-plugins"
+   STDOPT: +"-no-autoload-plugins" +"-machdep x86_64"
 */
 #include "stddef.h"
 int f(int b)
diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i
index 9570e109382c07d8d19a57248a384cbc372b9e66..1f69232742a7121f1642f1876d58490dc35bb608 100644
--- a/tests/syntax/logic_env.i
+++ b/tests/syntax/logic_env.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/logic_env_script.cmxs
-OPT: -load-module @PTEST_DIR@/logic_env_script
+ MODULE: logic_env_script
+   OPT: -no-autoload-plugins
 */
 
 //@ predicate foo(integer x) = x == 0;
diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i
index 8f08173f151e39627df74d38288858a1a2d9d68d..2a93071ea4d794e47a457e2eb32bbca80ddade3f 100644
--- a/tests/syntax/merge_loc.i
+++ b/tests/syntax/merge_loc.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/syntax/pp_lines.cmxs
-   STDOPT: #"-load-module tests/syntax/pp_lines.cmxs"
+ MODULE: pp_lines
+   STDOPT:
 */
 
 // Test locations when cabs2cil merges declarations and tentative definitions
diff --git a/tests/syntax/mutable_test.i b/tests/syntax/mutable_test.i
index 3c480aa053427eebf9bcf9ca6c5dcfd257cad058..a2c6ccc471ea7212683ad7c4f2232ec6d9010d56 100644
--- a/tests/syntax/mutable_test.i
+++ b/tests/syntax/mutable_test.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins -print
 */
 
 struct R_1 {
@@ -27,6 +27,3 @@ void f()
 {
   x.w.v.u.t.s.r = y;
 }
-
-
-
diff --git a/tests/syntax/reorder.i b/tests/syntax/reorder.i
index a611137930713ae5fbb4db09a2cbefdf59513905..2555be87b794ccfed63113536c3ec68bdc7b46e0 100644
--- a/tests/syntax/reorder.i
+++ b/tests/syntax/reorder.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT: -no-autoload-plugins
 */
 
 int x;
@@ -14,4 +14,3 @@ void f() { x++; }
 
 //@ requires Q: \let v = Q(255); !(!v||v) ;
 void g (void);
-
diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i
index 0b5e7a8bf6a82be6b854c63f410644568489c687..7061a2336c6de7c1009bd0ff14f57990274a38d6 100644
--- a/tests/syntax/syntactic_hook.i
+++ b/tests/syntax/syntactic_hook.i
@@ -1,7 +1,7 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
  EXIT: 1
-   STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+   STDOPT: +"-no-autoload-plugins"
 */
 
 
diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c
index 765e6bccedee2df52e4d8551c4fac28faa06523e..53903fc3d13e56edcb977d9b95c4455f784cecf6 100644
--- a/tests/syntax/temporary_location.c
+++ b/tests/syntax/temporary_location.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+   MODULE: @PTEST_NAME@
+   OPT: -print
 */
 
 int f(void) {
diff --git a/tests/syntax/transient_block.i b/tests/syntax/transient_block.i
index bfc8874399c9bb1e29a30b523ac5fbec9b52e77e..ed40f930bd9709d4612d4b25ec59ca31120fb8cc 100644
--- a/tests/syntax/transient_block.i
+++ b/tests/syntax/transient_block.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -kernel-warn-key transient-block=active
+ MODULE: @PTEST_NAME@
+   OPT: -kernel-warn-key transient-block=active
 */
 
 void f(void) { }
diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c
index 33a8d6c3537a3452d299e6a481c5514bbdb93022..37f3f89dbf588ced4590c9bb1c4a08bb7fc77178 100644
--- a/tests/syntax/typedef_multi_1.c
+++ b/tests/syntax/typedef_multi_1.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/typedef_multi.cmxs
-   OPT: -load-module @PTEST_DIR@/typedef_multi tests/syntax/typedef_multi_2.c
+ MODULE: typedef_multi
+   OPT: -no-autoload-plugins tests/syntax/typedef_multi_2.c
 */
 
 #include "tests/syntax/typedef_multi.h"
diff --git a/tests/syntax/vdescr_bts1387.i b/tests/syntax/vdescr_bts1387.i
index b20b1226bd2c890329ecea47201df49299e8f69b..8c041d8a3c3052ed3487e050230a1497dcb42814 100644
--- a/tests/syntax/vdescr_bts1387.i
+++ b/tests/syntax/vdescr_bts1387.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins
 */
 int f(int);
 int g(int);
diff --git a/tests/syntax/visit_create_local.i b/tests/syntax/visit_create_local.i
index 6d9a88989bca1c8106862f9bb5dd304b6da357c0..e49dc7c6da884dfd9e30f3162e8eaa1e9f469092 100644
--- a/tests/syntax/visit_create_local.i
+++ b/tests/syntax/visit_create_local.i
@@ -1,5 +1,5 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on bidon -print
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -then-on bidon -print
  */
 void main() { int x,y;  x = y; }
diff --git a/tests/value/unit_tests.i b/tests/value/unit_tests.i
index f480093ba099eda06a2fdca943402b02945c5cce..7cb38611d3a0c2ae466b20e6ee7bf17f9b0836d9 100644
--- a/tests/value/unit_tests.i
+++ b/tests/value/unit_tests.i
@@ -1,5 +1,5 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   MODULE: @PTEST_NAME@
    OPT:
 */
 /* run.config*