From fbdb744c3a00195c4b23f42bca74eb339a3dc3dc Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Wed, 30 Sep 2020 11:45:23 +0200 Subject: [PATCH] use MODULE directive instead of CMXS --- tests/cil/mkBinOp.i | 4 ++-- tests/misc/add_assigns.i | 4 ++-- tests/misc/bts0452.i | 4 ++-- tests/misc/bts0489.i | 4 ++-- tests/misc/bts1201.i | 4 ++-- tests/misc/bts1347.i | 4 ++-- tests/misc/callsite.i | 4 ++-- tests/misc/change_main.i | 4 ++-- tests/misc/cli_string_multiple_map.i | 4 ++-- tests/misc/copy_kf.i | 4 ++-- tests/misc/copy_machdep.i | 4 ++-- tests/misc/ensures.i | 4 ++-- tests/misc/exception.i | 6 +++--- tests/misc/global_decl_loc.i | 4 ++-- tests/misc/init_from_cil.i | 4 ++-- tests/misc/issue109.i | 4 ++-- tests/misc/justcopy.i | 4 ++-- tests/misc/keep_entry_point.i | 4 ++-- tests/misc/log-file.i | 4 ++-- tests/misc/log_twice.i | 4 ++-- tests/misc/remove_status_hyps.i | 4 ++-- tests/misc/static.i | 4 ++-- tests/misc/test_datatype.i | 4 ++-- tests/misc/version.i | 4 ++-- tests/misc/vis_queueInstr.i | 4 ++-- tests/misc/vis_spec.i | 4 ++-- tests/misc/visitor_creates_func_bts_1349.i | 4 ++-- tests/misc/well_typed_alarm.i | 4 ++-- tests/saveload/load_one.i | 4 ++-- tests/saveload/serialized_queue.i | 4 ++-- tests/spec/Extend.i | 4 ++-- tests/spec/Extend_short_print.i | 6 +++--- tests/spec/add_global.i | 4 ++-- tests/spec/bts0655.i | 4 ++-- tests/spec/comparison.i | 4 ++-- tests/spec/model.i | 4 ++-- tests/spec/pp_empty_spec.i | 4 ++-- tests/spec/property_test.i | 4 ++-- tests/spec/type_constructors_in_env.i | 4 ++-- tests/spec/type_of_term.i | 4 ++-- 40 files changed, 82 insertions(+), 82 deletions(-) diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i index f6d3c59d93a..f1565da600f 100644 --- a/tests/cil/mkBinOp.i +++ b/tests/cil/mkBinOp.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print -constfold +MODULE: @PTEST_NAME@.cmxs +STDOPT: +"-constfold" */ int main(void) { diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index d35203787a0..e61ecc871b3 100644 --- a/tests/misc/add_assigns.i +++ b/tests/misc/add_assigns.i @@ -1,7 +1,7 @@ /* run.config PLUGIN: report -CMXS: @PTEST_NAME@ -OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -then -report -then -print +MODULE: @PTEST_NAME@.cmxs +OPT: -then -report -then -print */ /*@ assigns *x; */ diff --git a/tests/misc/bts0452.i b/tests/misc/bts0452.i index a8eebfb6832..2ff6745a2a8 100644 --- a/tests/misc/bts0452.i +++ b/tests/misc/bts0452.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -typecheck -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: -typecheck */ /* must emit falls-through warning. */ int f (int foo, char** args) { diff --git a/tests/misc/bts0489.i b/tests/misc/bts0489.i index f920a1fc093..04714822f55 100644 --- a/tests/misc/bts0489.i +++ b/tests/misc/bts0489.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ typedef unsigned char uint8_t; diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i index fff261907b0..630683fb3d4 100644 --- a/tests/misc/bts1201.i +++ b/tests/misc/bts1201.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -eva-verbose 2 -load-module %{dep:@PTEST_NAME@.cmxs} -print + MODULE: @PTEST_NAME@.cmxs + OPT: -eva-verbose 2 -print */ void main() { //@ assert \true; } diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i index 9aa5ec357bb..b22939220f4 100644 --- a/tests/misc/bts1347.i +++ b/tests/misc/bts1347.i @@ -1,7 +1,7 @@ /* run.config PLUGIN: report - CMXS: @PTEST_NAME@ - OPT: @EVA_OPTIONS@ -load-module %{dep:@PTEST_NAME@.cmxs} -then -report + MODULE: @PTEST_NAME@.cmxs + OPT: @EVA_OPTIONS@ -then -report */ int f(int *x) { return *x; } int g(int *x) { return *(x++); } diff --git a/tests/misc/callsite.i b/tests/misc/callsite.i index ab6149b8732..57cec3316ab 100644 --- a/tests/misc/callsite.i +++ b/tests/misc/callsite.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ // Don't use -debug 1 option in the test command. diff --git a/tests/misc/change_main.i b/tests/misc/change_main.i index 627d22668d5..c24f0615a05 100644 --- a/tests/misc/change_main.i +++ b/tests/misc/change_main.i @@ -1,6 +1,6 @@ /* run.config* -CMXS: @PTEST_NAME@ -OPT: -eva -main f -load-module %{dep:@PTEST_NAME@.cmxs} -then-on change_main -main g -eva +MODULE: @PTEST_NAME@.cmxs +OPT: -eva -main f -then-on change_main -main g -eva */ int f(int x) { return x; } diff --git a/tests/misc/cli_string_multiple_map.i b/tests/misc/cli_string_multiple_map.i index 4c91d501d72..9d67683258a 100644 --- a/tests/misc/cli_string_multiple_map.i +++ b/tests/misc/cli_string_multiple_map.i @@ -1,4 +1,4 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -multiple-map a:1,b:2,a:3 + MODULE: @PTEST_NAME@.cmxs + OPT: -multiple-map a:1,b:2,a:3 */ diff --git a/tests/misc/copy_kf.i b/tests/misc/copy_kf.i index 245afeacb0b..14030a7a450 100644 --- a/tests/misc/copy_kf.i +++ b/tests/misc/copy_kf.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ /*@ requires \valid(p); assigns *p; ensures *p == x; */ diff --git a/tests/misc/copy_machdep.i b/tests/misc/copy_machdep.i index 704c0406024..b106aef20ae 100644 --- a/tests/misc/copy_machdep.i +++ b/tests/misc/copy_machdep.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -machdep x86_64 -enums int -no-unicode +MODULE: @PTEST_NAME@.cmxs +OPT: -machdep x86_64 -enums int -no-unicode */ int main () { return 0; } diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i index 41a96a18a21..66c76ecaae1 100644 --- a/tests/misc/ensures.i +++ b/tests/misc/ensures.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ //@ ensures *p==1; void main(int * p){ *p = 0; } diff --git a/tests/misc/exception.i b/tests/misc/exception.i index 16e3d60c420..7b5c3c93cea 100644 --- a/tests/misc/exception.i +++ b/tests/misc/exception.i @@ -1,7 +1,7 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -remove-exn -print + MODULE: @PTEST_NAME@.cmxs + OPT: -print + OPT: -remove-exn -print */ struct my_exn { int e; }; diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i index 704292f3104..6adb58636d2 100644 --- a/tests/misc/global_decl_loc.i +++ b/tests/misc/global_decl_loc.i @@ -1,5 +1,5 @@ /* run.config - CMXS: global_decl_loc - OPT: %{dep:global_decl_loc2.i} -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: %{dep:global_decl_loc2.i} */ int g; diff --git a/tests/misc/init_from_cil.i b/tests/misc/init_from_cil.i index e38ff8d3e44..1ca1be906ae 100644 --- a/tests/misc/init_from_cil.i +++ b/tests/misc/init_from_cil.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ int f(int x); diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i index 5f1c470e654..790aa603d9d 100644 --- a/tests/misc/issue109.i +++ b/tests/misc/issue109.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 */ void main() { int i, j = 0; diff --git a/tests/misc/justcopy.i b/tests/misc/justcopy.i index 33ffb04bc44..cad0fea6b95 100644 --- a/tests/misc/justcopy.i +++ b/tests/misc/justcopy.i @@ -1,4 +1,4 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ diff --git a/tests/misc/keep_entry_point.i b/tests/misc/keep_entry_point.i index b25fc87da1c..c99e1492bc4 100644 --- a/tests/misc/keep_entry_point.i +++ b/tests/misc/keep_entry_point.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -main f -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print +MODULE: @PTEST_NAME@.cmxs +OPT: -main f -print */ static int f(void); diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i index bff6e513cb3..38133efcea9 100644 --- a/tests/misc/log-file.i +++ b/tests/misc/log-file.i @@ -1,5 +1,5 @@ /* run.config - CMXS: plugin_log + MODULE: plugin_log.cmxs LOG: log-file-kernel-warnings.txt LOG: log-file-kernel-results.txt LOG: log-file-feedback.txt @@ -8,7 +8,7 @@ LOG: plugin-log-all.txt FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|' STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -eva-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -eva-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt" - OPT: -load-module plugin_log -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt + OPT: -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt DONTRUN: test disabled due to non-deterministic errors in CI */ int f(void); // generates kernel warning (missing spec) diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i index b4095c43f19..dc2306c1c6e 100644 --- a/tests/misc/log_twice.i +++ b/tests/misc/log_twice.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: @EVA_CONFIG@ -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: @EVA_CONFIG@ */ int* f() { diff --git a/tests/misc/remove_status_hyps.i b/tests/misc/remove_status_hyps.i index b62c85f1c6d..94c0702b8a5 100644 --- a/tests/misc/remove_status_hyps.i +++ b/tests/misc/remove_status_hyps.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ int main(void) { diff --git a/tests/misc/static.i b/tests/misc/static.i index bf9737025ee..26d56abf455 100644 --- a/tests/misc/static.i +++ b/tests/misc/static.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ int x; diff --git a/tests/misc/test_datatype.i b/tests/misc/test_datatype.i index 2de60116213..3b8208180d1 100644 --- a/tests/misc/test_datatype.i +++ b/tests/misc/test_datatype.i @@ -1,4 +1,4 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ diff --git a/tests/misc/version.i b/tests/misc/version.i index 55b838eefad..c9cc3e3277b 100644 --- a/tests/misc/version.i +++ b/tests/misc/version.i @@ -1,4 +1,4 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ diff --git a/tests/misc/vis_queueInstr.i b/tests/misc/vis_queueInstr.i index 1524969c741..d1113a9c095 100644 --- a/tests/misc/vis_queueInstr.i +++ b/tests/misc/vis_queueInstr.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print -then-on A -print +MODULE: @PTEST_NAME@.cmxs +OPT: -print -then-on A -print */ int main(){ diff --git a/tests/misc/vis_spec.i b/tests/misc/vis_spec.i index bd51666e947..dfb0db12d24 100644 --- a/tests/misc/vis_spec.i +++ b/tests/misc/vis_spec.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ //@ assigns \nothing; diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i index 21e906659f7..d49711b42c5 100644 --- a/tests/misc/visitor_creates_func_bts_1349.i +++ b/tests/misc/visitor_creates_func_bts_1349.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -load-script %{dep:@PTEST_NAME@.cmxs} -then-on test -print + MODULE: @PTEST_NAME@.cmxs + OPT: -then-on test -print */ int a = 10; diff --git a/tests/misc/well_typed_alarm.i b/tests/misc/well_typed_alarm.i index 83a2141b638..47649ab778f 100644 --- a/tests/misc/well_typed_alarm.i +++ b/tests/misc/well_typed_alarm.i @@ -1,6 +1,6 @@ /* run.config* -CMXS: @PTEST_NAME@ -OPT: -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ int main(int c) { int x = 0; diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i index 76c439e6ecb..2ff222cf2e6 100644 --- a/tests/saveload/load_one.i +++ b/tests/saveload/load_one.i @@ -1,7 +1,7 @@ /* run.config PLUGIN: sparecode - CMXS: @PTEST_NAME@ - STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs}" + MODULE: @PTEST_NAME@.cmxs + STDOPT: */ int G; diff --git a/tests/saveload/serialized_queue.i b/tests/saveload/serialized_queue.i index b5673fd361b..be2d8f6ca3e 100644 --- a/tests/saveload/serialized_queue.i +++ b/tests/saveload/serialized_queue.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ // empty C file, we're only interested in the script itself diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i index 5fe1d0b3a99..c6e161b7bd0 100644 --- a/tests/spec/Extend.i +++ b/tests/spec/Extend.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -copy -kernel-warn-key=annot-error=active +MODULE: @PTEST_NAME@.cmxs +OPT: -copy -kernel-warn-key=annot-error=active */ /*@ foo x == 0; diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i index ace4e346de6..7b3ae458f20 100644 --- a/tests/spec/Extend_short_print.i +++ b/tests/spec/Extend_short_print.i @@ -1,9 +1,9 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ /*@ without_short \true ; has_short \true ; -*/ \ No newline at end of file +*/ diff --git a/tests/spec/add_global.i b/tests/spec/add_global.i index 060e91bc160..755f2f64396 100644 --- a/tests/spec/add_global.i +++ b/tests/spec/add_global.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print +MODULE: @PTEST_NAME@.cmxs +OPT: -print */ int main () { return 0; } diff --git a/tests/spec/bts0655.i b/tests/spec/bts0655.i index 721f5b40377..3482676d722 100644 --- a/tests/spec/bts0655.i +++ b/tests/spec/bts0655.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ /*@ @ ensures \result == \max( a, b ); diff --git a/tests/spec/comparison.i b/tests/spec/comparison.i index 3efacf43f66..49629260c52 100644 --- a/tests/spec/comparison.i +++ b/tests/spec/comparison.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ /*@ predicate foo(boolean a, boolean b) = a == b; */ diff --git a/tests/spec/model.i b/tests/spec/model.i index 2d9b486e635..b44f80ec34b 100644 --- a/tests/spec/model.i +++ b/tests/spec/model.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" +MODULE: @PTEST_NAME@.cmxs +STDOPT: */ struct S { int x; int y; }; typedef struct S T; diff --git a/tests/spec/pp_empty_spec.i b/tests/spec/pp_empty_spec.i index 3f70a8fcfda..f53e09bad41 100644 --- a/tests/spec/pp_empty_spec.i +++ b/tests/spec/pp_empty_spec.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ int main(void) { int x = 0; diff --git a/tests/spec/property_test.i b/tests/spec/property_test.i index 328aeed5897..648ccb1b1af 100644 --- a/tests/spec/property_test.i +++ b/tests/spec/property_test.i @@ -1,6 +1,6 @@ /* run.config - CMXS: @PTEST_NAME@ - OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + MODULE: @PTEST_NAME@.cmxs + OPT: */ int X; diff --git a/tests/spec/type_constructors_in_env.i b/tests/spec/type_constructors_in_env.i index 97b266e4814..8ec7ff268b1 100644 --- a/tests/spec/type_constructors_in_env.i +++ b/tests/spec/type_constructors_in_env.i @@ -1,6 +1,6 @@ /* run.config -CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +MODULE: @PTEST_NAME@.cmxs +OPT: */ /*@ type foo = A | B; */ diff --git a/tests/spec/type_of_term.i b/tests/spec/type_of_term.i index 38c08465470..74f0b57316e 100644 --- a/tests/spec/type_of_term.i +++ b/tests/spec/type_of_term.i @@ -1,6 +1,6 @@ /* run.config - CMXS: Type_of_term - OPT: -load-module %{dep:Type_of_term.cmxs} -print + MODULE: @TEST_NAME@.cmxs + OPT: -print */ int t [42]; -- GitLab