[Tests] using SCRIPT directives

src/plugins/instantiate/tests/api/external_instantiator_registration.c

 /* 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){

src/plugins/instantiate/tests/plugin/needs_global.i

 /* 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) ;
 

src/plugins/report/tests/report/hyp.i

 /* 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; */
 }

src/plugins/report/tests/report/single.i

 /* 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() {

src/plugins/variadic/tests/declared/called_in_ghost.i

 /* 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, ...);
 

src/plugins/wp/tests/wp/stmtcompiler_test.i

 /* 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;

src/plugins/wp/tests/wp/stmtcompiler_test_rela.i

 /* 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;

src/plugins/wp/tests/wp_acsl/unsupported_builtin.i

 /* run.config
-
-  OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.ml
+  SCRIPT: @PTEST_NAME@
+  OPT:
 */
 /* run.config_qualif
   DONTRUN:

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;

tests/journal/control2.c

 /* 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++) {

tests/journal/intra.i

 /* 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:

tests/misc/global_decl_loc.i

 /* 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;

tests/misc/global_decl_loc2.i

 /* 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
 */