From b52baf872b1535b2ddf01dd6ca883410a08a42ea Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 12 Oct 2021 13:21:02 +0200
Subject: [PATCH] [Tests] more use of MODULE directive
---
tests/cil/change_to_instr.i | 3 ++-
tests/cil/queue_ghost_instr.i | 4 ++--
tests/misc/interpreted_automata_dataflow.i | 8 ++++----
tests/misc/pp_bin_hex.i | 3 ++-
tests/misc/pp_int.i | 5 +++--
tests/spec/Extend_recursive_preprocess.i | 4 ++--
tests/syntax/ghost_cv_var_decl.c | 4 ++--
7 files changed, 17 insertions(+), 14 deletions(-)
diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i
index b83b32608f6..dcf818affb8 100644
--- a/tests/cil/change_to_instr.i
+++ b/tests/cil/change_to_instr.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/cil/change_to_instr.ml -print
+MODULE: @PTEST_NAME@
+ OPT: -print
*/
diff --git a/tests/cil/queue_ghost_instr.i b/tests/cil/queue_ghost_instr.i
index 3bae2b6f40b..08e1a35e6d8 100644
--- a/tests/cil/queue_ghost_instr.i
+++ b/tests/cil/queue_ghost_instr.i
@@ -1,8 +1,8 @@
/* run.config
-OPT: -load-script tests/cil/queue_ghost_instr.ml -print
+ MODULE: @PTEST_NAME@
+ OPT: -print
*/
-
int main(){
int i = 0 ;
//@ ghost int j = 0 ;
diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i
index 29b72693389..6bb7034ce54 100644
--- a/tests/misc/interpreted_automata_dataflow.i
+++ b/tests/misc/interpreted_automata_dataflow.i
@@ -1,9 +1,9 @@
/* run.config
-LOG: @PTEST_NAME@_forward.dot
-LOG: @PTEST_NAME@_backward.dot
-OPT: -load-script @PTEST_DIR@/@PTEST_NAME@_forward.ml -load-script @PTEST_DIR@/@PTEST_NAME@_backward.ml
+MODULE: @PTEST_NAME@_forward @PTEST_NAME@_backward
+ LOG: @PTEST_NAME@_forward.dot
+ LOG: @PTEST_NAME@_backward.dot
+ OPT:
*/
-
/* Tests the dataflow functor of interpreted automata via a caml script
implementing a propagation of constants. */
diff --git a/tests/misc/pp_bin_hex.i b/tests/misc/pp_bin_hex.i
index a53499be699..eaea69c416c 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 tests/misc/pp_bin_hex.ml
+ MODULE: @PTEST_NAME@
+ OPT:
*/
diff --git a/tests/misc/pp_int.i b/tests/misc/pp_int.i
index d6da6546ebd..7c86337b7b5 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 tests/misc/pp_int.ml
+ COMMENT: test of Integer.pp_bin and Integer.pp_hex
+ MODULE: @PTEST_NAME@
+ OPT:
*/
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index ea7924d97db..146e898264f 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -1,6 +1,6 @@
/* run.config
-MODULE: @PTEST_NAME@
-OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
+ MODULE: @PTEST_NAME@
+ OPT: -kernel-warn-key=annot-error=active -print
*/
/*@ gl_foo foo1 {
diff --git a/tests/syntax/ghost_cv_var_decl.c b/tests/syntax/ghost_cv_var_decl.c
index 180192d7e25..c407d427b9c 100644
--- a/tests/syntax/ghost_cv_var_decl.c
+++ b/tests/syntax/ghost_cv_var_decl.c
@@ -1,9 +1,9 @@
/* run.config
-
EXIT: 1
OPT:-cpp-extra-args="-DFAIL_DECL_TYPE"
EXIT: 0
- OPT:-load-script @PTEST_DIR@/@PTEST_NAME@.ml
+ MODULE: @PTEST_NAME@
+ OPT:
*/
--
GitLab