diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index a6a820ecce977ef9f528f95bcb149fe3df18001a..18665b1b0e4bfdff1a28b8e42db78a97ebbcdb7a 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 1f3fc795582b79b21aad809bf852bfb655ce3cd7..ae10b78d66ad3175cb35f2bc8e575eab93d2e2e2 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 c33db7d4c1a3f7b4d29d0fc48a0aeaf37101775b..be4f1974355cf1d05007c7f2eac5687f616e2a5c 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 cbaf4a4e3d114ba17709f3f7fc7bfe0c6f8f5d27..dda5727fbcd2222c91dcb711d8d75098afd97857 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 5650e0651c86a321f57387978b130a56e1f889b6..2cb8c609baa0dfb5d506d7f24694408d1363f62e 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 a345a39f3b0ce1c51d4d918965de6620914abbde..8cb78b2e0e9b761068180caa17011420f4fefb7f 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 7dcfc493a8c89c38f1bb6189b0c562cccb8841e9..f78c94d2dab1080cf82abae2aa1af7d557c5933c 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 c6f70943352c91f4348680131c67bb9e27329040..374658f38ce3c2823acdbe90a413a4b8e17deb55 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 b4a7c3bc23730ae8b09c9d851046c6b3e300b520..f4491a4241f1ad4ec9d6faa47e54d8af6821909a 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 15fe7d6bc47b3ae91e25275f2bc159cebaeca86d..03e67db30b3abffdb30b9a31f198917c19894181 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 0b6f32f439f5a76fcda2d18135977d049f386d84..bddeea8fcceea8c6d52b1f93b051b1926094ce64 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 87979f0608b990d948997b250a3862bf51d98c48..6bd79189bb526ec401434d6ea32580373a48de73 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 ae04e6fb897e157311e2131e8c00117972aaa048..88df7e52cee82769532184b9ea77ea1b73d27644 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 a6e5006eb7dbab9286b39fbeaf6ea28e5c22be19..2a264e941a42580588fda014d923dce423534eb6 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 76cc35a53187fc9e58ea906527669b5a9482e117..a37807d2d13ad139afde7520a3e5a6b6e4dece38 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 7d767032b7e6c7ef1acc8f6a4a7e1ff655cab5f7..6439cfe960f1b443f80637d250d61da6004b0bd1 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 3d9d35c81d6a7ba665b909e1634f71e3af5289a6..4a6e475212ebf15e558888920e4c8e3600bc84fa 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 a345a39f3b0ce1c51d4d918965de6620914abbde..7591fbe17b2e5d871bdac304b8282f0ca7de513e 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 8cfd1982b8925ce6626f5d9b9d91594011759c5a..b290ec9ba542458c0f65ed51b1df14b00fb1c333 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 6ade640dbb8933cb359dac79d608f7acf33fc4d3..04f0fd4ee6c0e6dd6e7930b11dbd49e58d96a00c 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 833ee51da34f8228cc4ab373fe8573b430b7ca3f..498e4e0654ef12260798992d0ea71fcc66f73fd8 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 1c1ed1cb63f2918ef0516de494e301c62fd70f04..06a2ebcceeb318a91580fa7d4fb7bab6b922a72f 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 41d68823261de4e1003d19e22533dd438b4a7387..60ff5cbf50596aa9a9b245ce5781fc8da614e989 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 a436356626c8169ba8c349bf26bb5d2d31c72a52..1a3d33436554036277d24132d65fd9c868219f02 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 aaf7cccdef62fdaaaea56d6e6b5160163941eea4..cd627108a8efdc1f68d582e362dfc624f20eda43 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 b0863c3a2b3908f34f1bfe07919867975270aa3c..3a42cab18b65a8195f66d0a80ac3636cf45cb4cc 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 19405eb11ec4c3d5e608f535e9aeab5f595fb19a..be23d7c12680a0689865d201cedfe7a9e8b677f1 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 61fd2bb820de4616e9e18edfc2cd55a5eedd711b..4d5c8b78c9e2b75f510a82caa21541486cddcd19 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 c40858396b4be923663a262dc97a0cdc4b187771..da4a88c9898ea8c008c85a499bbcdb50bd533f0d 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 a03c0cd1c45050418effd185243b6dff7a1f7e3e..c292641a6e72f4b06d19a52000e78fb052d0aa19 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 236200877af3a87006d77bafa01de09eef090645..11ac1cd00a1cd0e5ec6f93c00a59b6e0e3ecc00c 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 82b35af07aafd25c3b780feed53159d006ff34a7..f9884778c87c760721d9a3f9616e909abe1f9ff0 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>