diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i index b83b32608f67b7918cae94834696592bc19cf770..dcf818affb809f75a6ebb3b8a5108127b4fe721f 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 3bae2b6f40b0ef3824806fb03117f9af8f5e9610..08e1a35e6d81cbcb8205855c69947c2f3e1aafd7 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 29b72693389a1bd791e5e8793002029fe0a6db06..6bb7034ce54e495ba8d3c345a0f2707e90aa50b0 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 a53499be69922b6d91cd0d4926968829ccf22a93..eaea69c416c9cf991051170e997763848f0029be 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 d6da6546ebd7eceeb7f3e589508b388adc949278..7c86337b7b53aeedc6dc54b188b768c913899175 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 ea7924d97dbe9d93159668c275655b2bee3e9f99..146e898264f6faf9ca1b6c6c661337c6684554f8 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 180192d7e258b1efa56107d775a19ae042dfee5b..c407d427b9c4feaaa9c790338a47b8aa8f7da522 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: */