diff --git a/src/plugins/instantiate/tests/api/external_instantiator_registration.c b/src/plugins/instantiate/tests/api/external_instantiator_registration.c index e7366b9816960b0eb6d3c2230c8ff45fc8827e79..465ff3e20be6ae56e53a6df0ce0ec17ce7c4e017 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 dfd53797477e08a50c44b80b06ea9743a7a73614..f5f1b9c687b7dea32045d9780f4c90493aa11648 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 8c448f2f02063d8dfc837607137387266ff1841f..44951ce35edf858ff80e9d5e4a45ab1449c8a3db 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 ee9b1b4359d8283a9ec3f48769c6e35c9462127d..b6b52f2180ef7f0c0080b1b423136f91030d244e 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 7d6ccc4f7f67ae5be501a3d5806fb645b6219623..65517dea7e669fd88d5eef741d90e8be999012a7 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 c610d54549272ce23c3610a5e58846880fcd5b00..35dda9748872dac9f50001077a5c5ca90bde797e 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 b206efad0519db1f347ae4a6b79e5221ff611f9d..2082e864d2ff04201c178e704b9fcabe5534b349 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 2c1a092d5a5046bb4cb1f64c8855c667c27d5a97..ef680942c150a77f92d05540c16cd2262f07e668 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 c18372e0716882a5fed2cab7451138cd9ac98841..f51a9bb5b161ca2b2a797be2f5ea34282763b314 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 0e3716b2ffb9aebe82488ec5eb7ab80b84850c8c..98470c1e45b7bcdfcdce05c9d3fb5ba8994f13cc 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 62c76b4a3a1de55491fbb25daae2f125bf2f36c7..95251316f0439ba2e13936850f9afd2a9f4a356a 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 e0f0ea85b89fcc58dd891952d708b4b99640979d..fa62d4ceac6358e50c5de95770dab53920a0f679 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 5f1867c879f6a4a75a417751a361c9e4e98a7cea..df106d00e7d9695253117182b3b2203bfd0f8287 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 */