From 81fbd5b4e5c2bc3528f4e198e81d6eb38848bc22 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 4 Dec 2020 15:36:36 +0100
Subject: [PATCH] [Tests] removing -load-script
---
ptests/ptests.ml | 2 +-
tests/cil/change_to_instr.i | 2 +-
tests/cil/queue_ghost_instr.i | 2 +-
tests/journal/control.i | 8 ++++----
tests/journal/control2.c | 6 +++---
tests/journal/intra.i | 4 ++--
tests/journal/oracle/control2_sav.res | 10 +++++-----
tests/misc/init_from_cil.i | 2 +-
tests/misc/interpreted_automata_dataflow.i | 3 ++-
tests/misc/pp_bin_hex.i | 3 ++-
tests/misc/pp_int.i | 3 ++-
tests/syntax/ghost_cv_var_decl.c | 4 ++--
12 files changed, 26 insertions(+), 23 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index db6de7e10f9..a21440216c9 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 6539a2560a2..8a087d5367e 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 9daed07fd9b..3b8144b67d6 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 4ffee833eda..578059556c8 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 2275978607c..2ef7bce9a8c 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 99aa4b66f12..11a12368cef 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 1734f9bb537..49bd1a6cf1d 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 64ea3362959..a07d9bf8d3c 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 94d7ec29751..f425059ea9e 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 7b267b69c49..2ee58479236 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 685adc627b4..3b32ffdd94f 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 fe95388feb3..14aa6aa2515 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 ;
--
GitLab