From 9abb2263fdd7278ea7981f779e3ebb3ffa8c965f Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Thu, 25 Mar 2021 12:30:13 +0100 Subject: [PATCH] [Tests] using MODULE directive into misc tests --- 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/bug_0209.c | 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/custom_machdep.c | 4 ++-- tests/misc/{custom_machdep => }/custom_machdep.ml | 0 tests/misc/ensures.i | 4 ++-- tests/misc/exception.i | 6 +++--- tests/misc/find_enclosing_loop.c | 4 ++-- tests/misc/init_from_cil.i | 4 ++-- tests/misc/issue109.i | 4 ++-- tests/misc/issue_191.c | 4 ++-- tests/misc/justcopy.i | 4 ++-- tests/misc/keep_entry_point.i | 4 ++-- tests/misc/log-file.i | 6 +++--- tests/misc/log_twice.i | 4 ++-- tests/misc/oracle/save_comments.res.oracle | 12 ++++++------ tests/misc/remove_status_hyps.i | 4 ++-- tests/misc/save_comments.i | 4 ++-- tests/misc/static.i | 4 ++-- tests/misc/test_datatype.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/misc/wstring_phase6.c | 4 ++-- 33 files changed, 70 insertions(+), 70 deletions(-) rename tests/misc/{custom_machdep => }/custom_machdep.ml (100%) diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index a6a820ecce9..18665b1b0e4 100644 --- a/tests/misc/add_assigns.i +++ b/tests/misc/add_assigns.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module report,@PTEST_DIR@/@PTEST_NAME@.cmxs -then -report -then -print + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module report -then -report -then -print */ /*@ assigns *x; */ diff --git a/tests/misc/bts0452.i b/tests/misc/bts0452.i index 1f3fc795582..ae10b78d66a 100644 --- a/tests/misc/bts0452.i +++ b/tests/misc/bts0452.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -typecheck -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -typecheck -no-autoload-plugins */ /* must emit falls-through warning. */ int f (int foo, char** args) { diff --git a/tests/misc/bts0489.i b/tests/misc/bts0489.i index c33db7d4c1a..be4f1974355 100644 --- a/tests/misc/bts0489.i +++ b/tests/misc/bts0489.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ typedef unsigned char uint8_t; diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i index cbaf4a4e3d1..dda5727fbcd 100644 --- a/tests/misc/bts1201.i +++ b/tests/misc/bts1201.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -eva-verbose 2 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print + MODULE: @PTEST_NAME@ + OPT: -eva-verbose 2 -print */ void main() { //@ assert \true; } diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i index 5650e0651c8..2cb8c609baa 100644 --- a/tests/misc/bts1347.i +++ b/tests/misc/bts1347.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -report + MODULE: @PTEST_NAME@ + OPT: @EVA_OPTIONS@ -then -report */ int f(int *x) { return *x; } int g(int *x) { return *(x++); } diff --git a/tests/misc/bug_0209.c b/tests/misc/bug_0209.c index a345a39f3b0..8cb78b2e0e9 100644 --- a/tests/misc/bug_0209.c +++ b/tests/misc/bug_0209.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ // Everything is done by the script diff --git a/tests/misc/callsite.i b/tests/misc/callsite.i index 7dcfc493a8c..f78c94d2dab 100644 --- a/tests/misc/callsite.i +++ b/tests/misc/callsite.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ // 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 c6f70943352..374658f38ce 100644 --- a/tests/misc/change_main.i +++ b/tests/misc/change_main.i @@ -1,6 +1,6 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -eva -main f -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on change_main -main g -eva + MODULE: @PTEST_NAME@ + 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 b4a7c3bc237..f4491a4241f 100644 --- a/tests/misc/cli_string_multiple_map.i +++ b/tests/misc/cli_string_multiple_map.i @@ -1,4 +1,4 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -multiple-map a:1,b:2,a:3 + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins -multiple-map a:1,b:2,a:3 */ diff --git a/tests/misc/copy_kf.i b/tests/misc/copy_kf.i index 15fe7d6bc47..03e67db30b3 100644 --- a/tests/misc/copy_kf.i +++ b/tests/misc/copy_kf.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ /*@ requires \valid(p); assigns *p; ensures *p == x; */ diff --git a/tests/misc/copy_machdep.i b/tests/misc/copy_machdep.i index 0b6f32f439f..bddeea8fcce 100644 --- a/tests/misc/copy_machdep.i +++ b/tests/misc/copy_machdep.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -machdep x86_64 -enums int -no-unicode + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins -machdep x86_64 -enums int -no-unicode */ int main () { return 0; } diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c index 87979f0608b..6bd79189bb5 100644 --- a/tests/misc/custom_machdep.c +++ b/tests/misc/custom_machdep.c @@ -1,8 +1,8 @@ /* run.config* EXIT: 1 - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.cmxs - OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-module @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@ -machdep custom -print -then -print + MODULE: @PTEST_NAME@.cmxs + OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep custom -print -then -print COMMENT: we need a -then to test double registering of a machdep */ #include "__fc_machdep_custom.h" diff --git a/tests/misc/custom_machdep/custom_machdep.ml b/tests/misc/custom_machdep.ml similarity index 100% rename from tests/misc/custom_machdep/custom_machdep.ml rename to tests/misc/custom_machdep.ml diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i index ae04e6fb897..88df7e52cee 100644 --- a/tests/misc/ensures.i +++ b/tests/misc/ensures.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: */ //@ ensures *p==1; void main(int * p){ *p = 0; } diff --git a/tests/misc/exception.i b/tests/misc/exception.i index a6e5006eb7d..2a264e941a4 100644 --- a/tests/misc/exception.i +++ b/tests/misc/exception.i @@ -1,7 +1,7 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -remove-exn -print + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins -print + OPT: -no-autoload-plugins -remove-exn -print */ struct my_exn { int e; }; diff --git a/tests/misc/find_enclosing_loop.c b/tests/misc/find_enclosing_loop.c index 76cc35a5318..a37807d2d13 100644 --- a/tests/misc/find_enclosing_loop.c +++ b/tests/misc/find_enclosing_loop.c @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ +OPT: -no-autoload-plugins */ void f () { diff --git a/tests/misc/init_from_cil.i b/tests/misc/init_from_cil.i index 7d767032b7e..6439cfe960f 100644 --- a/tests/misc/init_from_cil.i +++ b/tests/misc/init_from_cil.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ int f(int x); diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i index 3d9d35c81d6..4a6e475212e 100644 --- a/tests/misc/issue109.i +++ b/tests/misc/issue109.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 */ void main() { int i, j = 0; diff --git a/tests/misc/issue_191.c b/tests/misc/issue_191.c index a345a39f3b0..7591fbe17b2 100644 --- a/tests/misc/issue_191.c +++ b/tests/misc/issue_191.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ // Everything is done by the script diff --git a/tests/misc/justcopy.i b/tests/misc/justcopy.i index 8cfd1982b89..b290ec9ba54 100644 --- a/tests/misc/justcopy.i +++ b/tests/misc/justcopy.i @@ -1,4 +1,4 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ diff --git a/tests/misc/keep_entry_point.i b/tests/misc/keep_entry_point.i index 6ade640dbb8..04f0fd4ee6c 100644 --- a/tests/misc/keep_entry_point.i +++ b/tests/misc/keep_entry_point.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -main f -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print + MODULE: @PTEST_NAME@ + OPT: -main f -no-autoload-plugins -print */ static int f(void); diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i index 833ee51da34..498e4e0654e 100644 --- a/tests/misc/log-file.i +++ b/tests/misc/log-file.i @@ -1,14 +1,14 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/plugin_log.cmxs + FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|' LOG: log-file-kernel-warnings.txt LOG: log-file-kernel-results.txt LOG: log-file-feedback.txt LOG: log-file-value-all.txt LOG: log-file-value-default.txt 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 tests/misc/plugin_log -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt + MODULE: plugin_log + 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 1c1ed1cb63f..06a2ebcceeb 100644 --- a/tests/misc/log_twice.i +++ b/tests/misc/log_twice.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: @EVA_CONFIG@ -load-module @PTEST_DIR@/@PTEST_NAME@ + MODULE: @PTEST_NAME@ + OPT: @EVA_CONFIG@ */ int* f() { diff --git a/tests/misc/oracle/save_comments.res.oracle b/tests/misc/oracle/save_comments.res.oracle index 41d68823261..60ff5cbf505 100644 --- a/tests/misc/oracle/save_comments.res.oracle +++ b/tests/misc/oracle/save_comments.res.oracle @@ -2,8 +2,8 @@ Printing default project first time: /* Generated by Frama-C */ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments + MODULE: @PTEST_NAME@ + OPT: -keep-comments */ int f(void) { @@ -16,8 +16,8 @@ int f(void) Printing default project second time: /* Generated by Frama-C */ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments + MODULE: @PTEST_NAME@ + OPT: -keep-comments */ int f(void) { @@ -36,8 +36,8 @@ End of comments Printing saved project: /* Generated by Frama-C */ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments + MODULE: @PTEST_NAME@ + OPT: -keep-comments */ int f(void) { diff --git a/tests/misc/remove_status_hyps.i b/tests/misc/remove_status_hyps.i index a436356626c..1a3d3343655 100644 --- a/tests/misc/remove_status_hyps.i +++ b/tests/misc/remove_status_hyps.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ int main(void) { diff --git a/tests/misc/save_comments.i b/tests/misc/save_comments.i index aaf7cccdef6..cd627108a8e 100644 --- a/tests/misc/save_comments.i +++ b/tests/misc/save_comments.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments + MODULE: @PTEST_NAME@ + OPT: -keep-comments */ int f() { diff --git a/tests/misc/static.i b/tests/misc/static.i index b0863c3a2b3..3a42cab18b6 100644 --- a/tests/misc/static.i +++ b/tests/misc/static.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ +OPT: -no-autoload-plugins */ int x; diff --git a/tests/misc/test_datatype.i b/tests/misc/test_datatype.i index 19405eb11ec..be23d7c1268 100644 --- a/tests/misc/test_datatype.i +++ b/tests/misc/test_datatype.i @@ -1,4 +1,4 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ +OPT: -no-autoload-plugins */ diff --git a/tests/misc/vis_queueInstr.i b/tests/misc/vis_queueInstr.i index 61fd2bb820d..4d5c8b78c9e 100644 --- a/tests/misc/vis_queueInstr.i +++ b/tests/misc/vis_queueInstr.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -then-on A -print + MODULE: @PTEST_NAME@ +OPT: -no-autoload-plugins -print -then-on A -print */ int main(){ diff --git a/tests/misc/vis_spec.i b/tests/misc/vis_spec.i index c40858396b4..da4a88c9898 100644 --- a/tests/misc/vis_spec.i +++ b/tests/misc/vis_spec.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: -no-autoload-plugins */ //@ assigns \nothing; diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i index a03c0cd1c45..c292641a6e7 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 - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -then-on test -print + MODULE: @PTEST_NAME@ + 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 236200877af..11ac1cd00a1 100644 --- a/tests/misc/well_typed_alarm.i +++ b/tests/misc/well_typed_alarm.i @@ -1,6 +1,6 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + MODULE: @PTEST_NAME@ + OPT: */ int main(int c) { int x = 0; diff --git a/tests/misc/wstring_phase6.c b/tests/misc/wstring_phase6.c index 82b35af07aa..f9884778c87 100644 --- a/tests/misc/wstring_phase6.c +++ b/tests/misc/wstring_phase6.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -journal-disable -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -variadic-no-translation + MODULE: @PTEST_NAME@ + OPT: -journal-disable -print -variadic-no-translation */ #include <stdio.h> -- GitLab