From eaa5b27b8c268673f41e9fbdaae43ee1be2e67bb Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 21 Jan 2019 15:15:37 +0100
Subject: [PATCH] [tests] nomalized use of -load-module option

---
 tests/builtins/Longinit_sequencer.i |  4 ++--
 tests/callgraph/function_pointer.i  |  8 ++++----
 tests/cil/mkBinOp.i                 |  2 +-
 tests/journal/intra.i               |  4 ++--
 tests/misc/copy_kf.i                |  2 +-
 tests/misc/copy_machdep.i           |  2 +-
 tests/misc/exception.i              |  4 ++--
 tests/misc/global_decl_loc.i        |  2 +-
 tests/misc/my_visitor.c             |  2 +-
 tests/saveload/basic.i              | 10 +++++-----
 tests/saveload/multi_project.i      |  6 +++---
 tests/slicing/adpcm.c               |  4 ++--
 tests/slicing/combine.i             |  4 ++--
 tests/slicing/ex_spec_interproc.i   |  4 ++--
 tests/slicing/horwitz.i             | 10 +++++-----
 tests/slicing/mark_all_slices.i     |  4 ++--
 tests/slicing/merge.i               |  4 ++--
 tests/slicing/min_call.i            |  4 ++--
 tests/slicing/select_by_annot.i     |  4 ++--
 tests/slicing/select_simple.i       |  4 ++--
 tests/slicing/simple_intra_slice.i  |  4 ++--
 tests/slicing/slice_no_body.i       |  4 ++--
 tests/slicing/switch.i              |  4 ++--
 tests/spec/Extend.i                 |  2 +-
 tests/syntax/Refresh_visitor.i      |  2 +-
 tests/syntax/formals_decl_leak.i    |  2 +-
 26 files changed, 53 insertions(+), 53 deletions(-)

diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i
index 2998da18c7d..9545fae2592 100644
--- a/tests/builtins/Longinit_sequencer.i
+++ b/tests/builtins/Longinit_sequencer.i
@@ -1,4 +1,4 @@
 /* run.config*
-EXECNOW: make tests/builtins/Longinit_sequencer.cmxs
-OPT: -load-module tests/builtins/Longinit_sequencer.cmxs -eva-show-progress -res-file @PTEST_RESULT@
+EXECNOW: make @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -res-file @PTEST_RESULT@
 */
diff --git a/tests/callgraph/function_pointer.i b/tests/callgraph/function_pointer.i
index be249adbd33..27202a3c7ff 100644
--- a/tests/callgraph/function_pointer.i
+++ b/tests/callgraph/function_pointer.i
@@ -1,10 +1,10 @@
 /* run.config
    COMMENT: Test option -cg-function-pointers
    EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -cg-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@
-   OPT: -cg-no-services -cg-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@
-   OPT: -cg-no-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@
-   OPT: -cg-no-services -cg-no-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@
+   OPT: -cg-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -cg-no-services -cg-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -cg-no-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -cg-no-services -cg-no-function-pointers -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
 */
 
 int (*fptr)(int);
diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i
index caa9dd0c396..64f2a643d8c 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: -load-module @PTEST_DIR@/@PTEST_NAME@ -print -constfold
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold
 */
 
 int main(void) {
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 07b7d59e05d..dea5fdbface 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@ -journal-enable -journal-name tests/journal/result/intra_journal.ml tests/journal/intra.i > /dev/null 2> /dev/null
-   CMD: @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@
+   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
    OPT: -load-script tests/journal/result/intra_journal -journal-disable
 */
 
diff --git a/tests/misc/copy_kf.i b/tests/misc/copy_kf.i
index 029cbd00d67..f5d849a3384 100644
--- a/tests/misc/copy_kf.i
+++ b/tests/misc/copy_kf.i
@@ -1,6 +1,6 @@
 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
 */
 
 /*@ requires \valid(p); assigns *p; ensures *p == x; */
diff --git a/tests/misc/copy_machdep.i b/tests/misc/copy_machdep.i
index 3c150a094ff..cfc77294f14 100644
--- a/tests/misc/copy_machdep.i
+++ b/tests/misc/copy_machdep.i
@@ -1,6 +1,6 @@
 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -machdep x86_64 -enums int -no-unicode
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -machdep x86_64 -enums int -no-unicode
 */
 
 int main () { return 0; }
diff --git a/tests/misc/exception.i b/tests/misc/exception.i
index 4b73ec77664..1c10993b286 100644
--- a/tests/misc/exception.i
+++ b/tests/misc/exception.i
@@ -1,7 +1,7 @@
 /* run.config
    EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -print
-   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -remove-exn -print
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -remove-exn -print
  */
 struct my_exn { int e; };
 
diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i
index 3da30326dde..62de46c9540 100644
--- a/tests/misc/global_decl_loc.i
+++ b/tests/misc/global_decl_loc.i
@@ -1,4 +1,4 @@
 /* run.config
-   OPT: @PTEST_DIR@/global_decl_loc2.i -load-module @PTEST_DIR@/global_decl_loc.cmxs
+   OPT: @PTEST_DIR@/global_decl_loc2.i -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
  */
 int g;
diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c
index 921a82c24c4..ce79f9d6fd4 100644
--- a/tests/misc/my_visitor.c
+++ b/tests/misc/my_visitor.c
@@ -1,6 +1,6 @@
 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav FRAMAC_PLUGIN=./lib/plugins @frama-c@ @PTEST_FILE@ -load-module @PTEST_DIR@/@PTEST_NAME@ -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@_sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@_sav.err
+EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav FRAMAC_PLUGIN=./lib/plugins @frama-c@ @PTEST_FILE@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@_sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@_sav.err
 OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -print
 */
 int f() {
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index 3b6a7040f34..0a37b04868e 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,12 +1,12 @@
 /* run.config
-   EXECNOW: make -s ./@PTEST_DIR@/@PTEST_NAME@.cmxs
-   EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@ -eva -out -input -deps -eva-show-progress ./tests/saveload/basic.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
-   EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav ./@PTEST_DIR@/@PTEST_NAME@.i -eva -out -input -deps -eva-show-progress > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva -out -input -deps -eva-show-progress ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
+   EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva -out -input -deps -eva-show-progress > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
    OPT: -load ./tests/saveload/result/basic.sav -eva -out -input -deps -journal-disable
-   CMD: @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@
+   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
+   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
    OPT: -load ./tests/saveload/result/status.sav
 */
diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i
index b3a6c55cc1b..e8c3589515c 100644
--- a/tests/saveload/multi_project.i
+++ b/tests/saveload/multi_project.i
@@ -1,8 +1,8 @@
 /* run.config
-   EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav -eva-show-progress -semantic-const-folding ./tests/saveload/multi_project.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
-   EXECNOW: make -s ./tests/saveload/multi_project.cmxs
+   EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav -eva-show-progress -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -load ./tests/saveload/result/multi_project.sav -journal-disable
-   CMD: @frama-c@ -load-module ./tests/saveload/multi_project
+   CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva -eva-show-progress
 */
 int f(int x) {
diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c
index 3ca387a3406..88dbc4dbda0 100644
--- a/tests/slicing/adpcm.c
+++ b/tests/slicing/adpcm.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/adpcm.cmxs
-   OPT: -eva-show-progress -load-module ./tests/slicing/libSelect.cmxs -load-module ./tests/slicing/adpcm.cmxs -ulevel -1 -deps -slicing-level 2 -journal-disable
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -eva-show-progress -load-module ./tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -ulevel -1 -deps -slicing-level 2 -journal-disable
 */
 
 #include "tests/test/adpcm.c"
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 983a97af140..16d12c1adcd 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/combine.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/combine.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -journal-disable
 */
 
diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i
index 9f6d8ca1360..962dd869e61 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/ex_spec_interproc.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/ex_spec_interproc.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -journal-disable
 */
 
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 3cc83fb2dd7..0178857313f 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -1,12 +1,12 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/horwitz.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/horwitz.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -slicing-level 0 -journal-disable
 */
 
-/* bin/toplevel.opt -deps -eva tests/slicing/horwitz.c */
-/* bin/toplevel.opt -deps -pdg-debug -pdg tests/slicing/horwitz.c */
-/* cf aussi tests/slicing/horwitz.ml */
+/* bin/toplevel.opt -deps -eva @PTEST_DIR@/@PTEST_NAME@.c */
+/* bin/toplevel.opt -deps -pdg-debug -pdg @PTEST_DIR@/@PTEST_NAME@.c */
+/* cf aussi @PTEST_DIR@/@PTEST_NAME@.ml */
 
 int add (int a, int b) {
   return a+b;
diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index 3454c9e2bef..d2581222659 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/mark_all_slices.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/mark_all_slices.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -slicing-level 3 -no-slice-callers -journal-disable
 */
 int A, B, C, D;
diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i
index b25108129ad..bf0509784e3 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/merge.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module tests/slicing/merge.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -slicing-level 3 -journal-disable
 */
 
diff --git a/tests/slicing/min_call.i b/tests/slicing/min_call.i
index bb033d1fc63..f7cc89e6a8d 100644
--- a/tests/slicing/min_call.i
+++ b/tests/slicing/min_call.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/min_call.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/min_call.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -lib-entry -main g -journal-disable -slicing-level 3
 */
 
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index fe285f2541c..a0cd4471cf1 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/select_by_annot.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/select_by_annot.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -lib-entry -main main -journal-disable
    CMD: bin/toplevel.opt
    OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.i
index 9e30123cd9b..9883f3ff583 100644
--- a/tests/slicing/select_simple.i
+++ b/tests/slicing/select_simple.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/select_simple.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/select_simple.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -journal-disable
 */
 
diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i
index 06511100033..e335e824fe8 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/simple_intra_slice.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/simple_intra_slice.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -no-slice-callers -journal-disable 
 */
 int Unknown;
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index 0f261cfc5c8..9c249f20d9f 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s tests/slicing/slice_no_body.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/slice_no_body.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -lib-entry -main h -journal-disable
 */
 
diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i
index 11e453ccb71..0b1ca36ce07 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,6 +1,6 @@
 /*  run.config
-   EXECNOW: make -s tests/slicing/switch.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/switch.cmxs
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT: -eva-show-progress -deps -journal-disable
 */
 int main (char choix) {
diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index dd42b218070..fc594736698 100644
--- a/tests/spec/Extend.i
+++ b/tests/spec/Extend.i
@@ -1,6 +1,6 @@
 /* run.config
 EXECNOW: make @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -copy -kernel-warn-key=annot-error=active
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -copy -kernel-warn-key=annot-error=active
 */
 
 /*@ foo x == 0;
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index 07ebc38f1b1..0786760a68f 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@ -eva-show-progress
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress
 */
 
 struct S { int i; };
diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i
index f7167558fe3..f1e96e698a8 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 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs tests/syntax/formals_decl_leak_1.i
+OPT: -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @PTEST_DIR@/@PTEST_NAME@_1.i
 */
 
 void f(int x);
-- 
GitLab