diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index db6de7e10f9f38d3a8a50620a0ea96835ae3e38d..a21440216c951d8e8656b2d4e0d6c64692f54c03 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -941,7 +941,7 @@ let command_string ~result_fmt ~oracle_fmt command =
| Some _ -> (log_prefix ^ ".res.unfiltered-log"),(log_prefix ^ ".err.unfiltered-log")
in
let deps = command.deps in
- let accepted_exit_code = Format.sprintf "with-accepted-exit-codes (or %d 1 4 125)" command.exit_code in
+ let accepted_exit_code = Format.sprintf "with-accepted-exit-codes (or %d 1 4)" command.exit_code in
let command_string = basic_command_string command in
Format.fprintf result_fmt
"(rule ; TEST #%d OF TEST FILE %S\n \
diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i
index 6539a2560a2599cbec14b19e35771b8e33255ffa..8a087d5367ee71c19273b34e15af6e33576d26a9 100644
--- a/tests/cil/change_to_instr.i
+++ b/tests/cil/change_to_instr.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -load-script %{dep:change_to_instr.ml} -print
+MODULE: @PTEST_NAME@
*/
diff --git a/tests/cil/queue_ghost_instr.i b/tests/cil/queue_ghost_instr.i
index 9daed07fd9b2412221e776c1254a9f69450e391b..3b8144b67d6d6809834fd4ebe282360c01f4b4af 100644
--- a/tests/cil/queue_ghost_instr.i
+++ b/tests/cil/queue_ghost_instr.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -load-script %{dep:queue_ghost_instr.ml} -print
+MODULE: @PTEST_NAME@
*/
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 4ffee833edadb4ce3fa17e5f62cceb05acd7af8c..578059556c885c97b1e27703c2d7134d15dd28d7 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,16 +1,16 @@
/* run.config
COMMENT: do not compare generated journals since they depend on current time
- CMXS: abstract_cpt use_cpt
+ CMXS: abstract_cpt use_cpt control_journal control_journal_bis abstract_cpt_journal
EXECNOW: BIN control_journal.ml @frama-c@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name control_journal.ml > /dev/null 2> /dev/null
- OPT: -load-script %{dep:control_journal.ml}
+ OPT: -load-module %{dep:control_journal.cmxs}
EXECNOW: BIN control_journal_bis.ml cp %{dep:control_journal.ml} control_journal_bis.ml > /dev/null 2> /dev/null
- OPT: -load-script %{dep:control_journal_bis.ml} -calldeps
+ OPT: -load-module %{dep:control_journal_bis.cmxs} -calldeps
EXECNOW: BIN abstract_cpt_journal.ml @frama-c-cmd@ -journal-enable -load-module %{dep:abstract_cpt.cmxs} -load-module %{dep:use_cpt.cmxs} -journal-name abstract_cpt_journal.ml > /dev/null 2> /dev/null
- OPT: -load-script %{dep:abstract_cpt_journal.ml} -load-module %{dep:abstract_cpt.cmxs} -load-module %{dep:use_cpt.cmxs}
+ OPT: -load-module %{dep:abstract_cpt_journal.cmxs} -load-module %{dep:abstract_cpt.cmxs} -load-module %{dep:use_cpt.cmxs}
*/
int x,y,c,d;
void f() {
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 2275978607c482c51d8b26dee9514ab085fc7591..2ef7bce9a8c1d9f5e0a1614ea2710190f3c52c5f 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,12 +1,12 @@
/* run.config
+ CMXS: control_journal_next2 control_journal2
EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml > /dev/null 2> /dev/null
- EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -load-script %{dep:control_journal2.ml} -lib-entry -journal-name control_journal_next2.ml > control2_sav.res 2> control2_sav.err
+ EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -load-module %{dep:control_journal2.cmxs} -lib-entry -journal-name control_journal_next2.ml > control2_sav.res 2> control2_sav.err
PLUGIN: callgraph @EVA_CONFIG@
- OPT: -load-script %{dep:control_journal_next2.ml}
+ OPT: -load-module %{dep:control_journal_next2.cmxs}
*/
/* The last OPT was testing reading from byte when generated from native */
-
int x,y,c,d;
void f() {
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 99aa4b66f1254b7d923ba00adbfe06168e94dafe..11a12368cefe9a2a6f78da8fcb1203d9c1d6b71a 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,9 +1,9 @@
/* run.config
PLUGIN: sparecode @EVA_CONFIG@
- CMXS: @PTEST_NAME@
+ CMXS: @PTEST_NAME@ intra_journal
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name intra_journal.ml > /dev/null 2> /dev/null
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} @OPTIONS@
- OPT: -load-script %{dep:intra_journal.ml} -journal-disable
+ OPT: -load-module %{dep:intra_journal.cmxs} -journal-disable
*/
/* Waiting for results such as:
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index 1734f9bb5372539b42ca6899a554625e521d5272..49bd1a6cf1d68bfe0f22d3fd3484ad1bfbc73641 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control2.c:14: starting to merge loop iterations
-[eva:alarm] control2.c:17: Warning:
+[eva] control2.c:15: starting to merge loop iterations
+[eva:alarm] control2.c:18: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -38,11 +38,11 @@
y ∈ [--..--]
c ∈ [--..--]
d ∈ [--..--]
-[eva:alarm] control2.c:15: Warning:
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:17: Warning:
+[eva:alarm] control2.c:18: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/misc/init_from_cil.i b/tests/misc/init_from_cil.i
index 64ea3362959705d9fa9fb5291e8f1b31cd0453d4..a07d9bf8d3c387982eef2db63c05038bd7f6e840 100644
--- a/tests/misc/init_from_cil.i
+++ b/tests/misc/init_from_cil.i
@@ -1,6 +1,6 @@
/* run.config
MODULE: @PTEST_NAME@
- OPT:
+ OPT:
*/
int f(int x);
diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i
index 94d7ec297518c1447a14375bf1c998b855018275..f425059ea9e10b88b3845cb07824227b7f9ecd1c 100644
--- a/tests/misc/interpreted_automata_dataflow.i
+++ b/tests/misc/interpreted_automata_dataflow.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script %{dep:interpreted_automata_dataflow.ml}
+MODULE: @PTEST_NAME@
+OPT:
*/
/* Tests the dataflow functor of interpreted automata via a caml script
diff --git a/tests/misc/pp_bin_hex.i b/tests/misc/pp_bin_hex.i
index 7b267b69c498e4bef6182abd049b7922444b8bc6..2ee58479236ec01b13e72b5ea62f46090d697926 100644
--- a/tests/misc/pp_bin_hex.i
+++ b/tests/misc/pp_bin_hex.i
@@ -1,3 +1,4 @@
/* run.config
- OPT: -no-autoload-plugins -load-script %{dep:pp_bin_hex.ml}
+ MODULE: @PTEST_NAME@
+ OPT:
*/
diff --git a/tests/misc/pp_int.i b/tests/misc/pp_int.i
index 685adc627b4a0e8f4d158ab913623898247ce6a8..3b32ffdd94fc2893538f8d736aa4c7b17bf3abd0 100644
--- a/tests/misc/pp_int.i
+++ b/tests/misc/pp_int.i
@@ -1,4 +1,5 @@
/* run.config
COMMENT: test of Integer.pp_bin and Integer.pp_hex
- OPT: -load-script %{dep:pp_int.ml}
+ MODULE: @PTEST_NAME@
+ OPT:
*/
diff --git a/tests/syntax/ghost_cv_var_decl.c b/tests/syntax/ghost_cv_var_decl.c
index fe95388feb3fabddac2438fa92151e376ebaaf9b..14aa6aa2515faefdb118df45d2820a7c75c56d8a 100644
--- a/tests/syntax/ghost_cv_var_decl.c
+++ b/tests/syntax/ghost_cv_var_decl.c
@@ -1,9 +1,9 @@
/* run.config
+ CMXS: @PTEST_NAME@
OPT:-cpp-extra-args="-DFAIL_DECL_TYPE"
- OPT:-load-script %{dep:@PTEST_NAME@.ml}
+ OPT:-load-module %{dep:@PTEST_NAME@.cmxs}
*/
-
/* When there is no comment, the code should be allowed */
void f_ints(){
int ng ;