From 444a4a7e9cba21f467a8ded4455d19e8910aa414 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 13 Oct 2021 12:04:21 +0200
Subject: [PATCH] [Tests] using SCRIPT directives
---
.../tests/api/external_instantiator_registration.c | 4 ++--
src/plugins/instantiate/tests/plugin/needs_global.i | 4 ++--
.../plugin/{needs_globals.ml => needs_global.ml} | 0
src/plugins/report/tests/report/hyp.i | 8 ++++----
src/plugins/report/tests/report/single.i | 9 ++++++---
.../variadic/tests/declared/called_in_ghost.i | 4 ++--
src/plugins/wp/tests/wp/stmtcompiler_test.i | 4 ++--
src/plugins/wp/tests/wp/stmtcompiler_test_rela.i | 4 ++--
src/plugins/wp/tests/wp_acsl/unsupported_builtin.i | 4 ++--
tests/journal/control.i | 10 +++++++---
tests/journal/control2.c | 12 ++++++------
tests/journal/intra.i | 6 +++---
tests/misc/global_decl_loc.i | 4 +++-
tests/misc/global_decl_loc2.i | 3 ++-
14 files changed, 43 insertions(+), 33 deletions(-)
rename src/plugins/instantiate/tests/plugin/{needs_globals.ml => needs_global.ml} (100%)
diff --git a/src/plugins/instantiate/tests/api/external_instantiator_registration.c b/src/plugins/instantiate/tests/api/external_instantiator_registration.c
index e7366b98169..465ff3e20be 100644
--- a/src/plugins/instantiate/tests/api/external_instantiator_registration.c
+++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -load-script tests/api/external_instantiator_registration.ml -instantiate -check -print
+ SCRIPT: @PTEST_NAME@
+ OPT: -instantiate -check -print
*/
-
void mine(void* parameter) ;
void foo(void){
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.i b/src/plugins/instantiate/tests/plugin/needs_global.i
index dfd53797477..f5f1b9c687b 100644
--- a/src/plugins/instantiate/tests/plugin/needs_global.i
+++ b/src/plugins/instantiate/tests/plugin/needs_global.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -load-script tests/plugin/needs_globals.ml -instantiate -check -print
+ SCRIPT: @PTEST_NAME@
+ OPT: -instantiate -check -print
*/
-
int i ; // needed for already_one specifciation
void already_one(void* parameter) ;
diff --git a/src/plugins/instantiate/tests/plugin/needs_globals.ml b/src/plugins/instantiate/tests/plugin/needs_global.ml
similarity index 100%
rename from src/plugins/instantiate/tests/plugin/needs_globals.ml
rename to src/plugins/instantiate/tests/plugin/needs_global.ml
diff --git a/src/plugins/report/tests/report/hyp.i b/src/plugins/report/tests/report/hyp.i
index 8c448f2f020..44951ce35ed 100644
--- a/src/plugins/report/tests/report/hyp.i
+++ b/src/plugins/report/tests/report/hyp.i
@@ -1,11 +1,11 @@
/* run.config
- OPT: -load-script tests/report/one_hyp.ml
- OPT: -load-script tests/report/several_hyps.ml
+ SCRIPT: one_hyp
+ OPT:
+ SCRIPT: several_hyps
+ OPT:
*/
-
void f(void);
void f2(void);
-
void g() {
/*@ assert \true; */
}
diff --git a/src/plugins/report/tests/report/single.i b/src/plugins/report/tests/report/single.i
index ee9b1b4359d..b6b52f2180e 100644
--- a/src/plugins/report/tests/report/single.i
+++ b/src/plugins/report/tests/report/single.i
@@ -1,7 +1,10 @@
/* run.config
- OPT: -load-script tests/report/projectified_status.ml
- OPT: -load-script tests/report/no_hyp.ml
- OPT: -load-script tests/report/multi_emitters.ml
+ SCRIPT: projectified_status
+ OPT:
+ SCRIPT: no_hyp
+ OPT:
+ SCRIPT: multi_emitters
+ OPT:
*/
void main() {
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.i b/src/plugins/variadic/tests/declared/called_in_ghost.i
index 7d6ccc4f7f6..65517dea7e6 100644
--- a/src/plugins/variadic/tests/declared/called_in_ghost.i
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -kernel-warn-key ghost:bad-use=inactive -load-script tests/declared/called_in_ghost.ml -print
+ SCRIPT: @PTEST_NAME@
+ OPT: -kernel-warn-key ghost:bad-use=inactive -print
*/
// Note: we deactivate "ghost:bad-use" to check that printing goes right
-
/*@ assigns \nothing ; */
void function(int e, ...);
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index c610d545492..35dda974887 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key shell
+ SCRIPT: @PTEST_NAME@
+ OPT: -wp-msg-key shell
*/
-
int empty (int c){
/*@ assert \true; */
return c;
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index b206efad051..2082e864d2f 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key shell
+ SCRIPT: @PTEST_NAME@
+ OPT: -wp-msg-key shell
*/
-
int empty (int c){
c = c < 0 ? c + 10 : c+100;
int tmp;
diff --git a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i
index 2c1a092d5a5..ef680942c15 100644
--- a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i
+++ b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i
@@ -1,6 +1,6 @@
/* run.config
-
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.ml
+ SCRIPT: @PTEST_NAME@
+ OPT:
*/
/* run.config_qualif
DONTRUN:
diff --git a/tests/journal/control.i b/tests/journal/control.i
index c18372e0716..f51a9bb5b16 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -2,13 +2,17 @@
COMMENT: do not compare generated journals since they depend on current time
PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- OPT: -load-script @PTEST_RESULT@/control_journal.ml
+ SCRIPT: result/control_journal.ml
+ OPT:
MODULE:
+ SCRIPT: result/control_journal_bis.ml
EXECNOW: BIN control_journal_bis.ml cp @PTEST_RESULT@/control_journal.ml @PTEST_RESULT@/control_journal_bis.ml > @DEV_NULL@ 2> @DEV_NULL@
- OPT: -calldeps -load-script @PTEST_RESULT@/control_journal_bis.ml
+ OPT: -calldeps
MODULE: abstract_cpt use_cpt
+ SCRIPT:
EXECNOW: BIN abstract_cpt_journal.ml @frama-c@ -journal-enable -journal-name @PTEST_RESULT@/abstract_cpt_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- OPT: -load-script @PTEST_RESULT@/abstract_cpt_journal.ml
+ SCRIPT: result/abstract_cpt_journal.ml
+ OPT:
*/
int x,y,c,d;
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 0e3716b2ffb..98470c1e45b 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,12 +1,12 @@
/* run.config
- EXECNOW: BIN control_journal2.ml ./bin/toplevel.opt -journal-enable -eva -deps -out -main f -journal-name tests/journal/result/control_journal2.ml tests/journal/control2.c > @DEV_NULL@ 2> @DEV_NULL@
- EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script tests/journal/result/control_journal2 -lib-entry -journal-name tests/journal/result/control_journal_next2.ml tests/journal/control2.c > ./tests/journal/result/control2_sav.res 2> ./tests/journal/result/control2_sav.err
- CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script tests/journal/result/control_journal_next2
+ PLUGIN: @EVA_PLUGINS@
+ EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
+ SCRIPT: result/control_journal2
+ EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -lib-entry -journal-name @PTEST_RESULT@/control_journal_next2.ml @PTEST_FILE@ > @PTEST_RESULT@/control2_sav.res 2> @PTEST_RESULT@/control2_sav.err
+ SCRIPT: result/control_journal_next2
+ OPT:
*/
-
int x,y,c,d;
-
void f() {
int i;
for(i=0; i<4 ; i++) {
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 62c76b4a3a1..95251316f04 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,9 +1,9 @@
/* run.config
PLUGIN: @EVA_PLUGINS@ sparecode
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
+ EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
+ SCRIPT: result/intra_journal
+ OPT:
*/
/* Waiting for results such as:
diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i
index e0f0ea85b89..fa62d4ceac6 100644
--- a/tests/misc/global_decl_loc.i
+++ b/tests/misc/global_decl_loc.i
@@ -1,5 +1,7 @@
/* run.config
- MODULE: global_decl_loc
+ COMMENT: the script "global_decl_loc.ml" is also used by the test "global_decl_loc2.i"
+ SCRIPT: global_decl_loc
OPT: @PTEST_DIR@/global_decl_loc2.i
*/
+
int g;
diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i
index 5f1867c879f..df106d00e7d 100644
--- a/tests/misc/global_decl_loc2.i
+++ b/tests/misc/global_decl_loc2.i
@@ -1,5 +1,6 @@
/* run.config*
- MODULE: global_decl_loc
+ COMMENT: the script "global_decl_loc.ml" is also used by the test "global_decl_loc.i"
+ SCRIPT: global_decl_loc
OPT: @PTEST_DIR@/global_decl_loc.i
*/
--
GitLab