From 01f76fceb6c7a242782aa6b4c2733fe9e8c58ca7 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 25 Mar 2021 09:50:19 +0100
Subject: [PATCH] [Tests] using MODULE directive
---
src/plugins/aorai/tests/ya/assigns.c | 2 +-
tests/cil/insert_formal.i | 2 +-
tests/cil/mkBinOp.i | 4 ++--
.../introduction_of_non_explicit_cast.c | 4 ++--
tests/float/fval_test.i | 2 +-
tests/journal/intra.i | 6 +++---
tests/misc/behavior_names.i | 2 +-
tests/misc/debug_category.i | 2 +-
tests/misc/filepath.i | 4 ++--
tests/misc/version.i | 2 +-
tests/pdg/sets.c | 4 ++--
tests/scope/bts971.c | 4 ++--
tests/scope/zones.c | 2 +-
tests/spec/Extend.i | 4 ++--
tests/spec/Extend_preprocess.i | 2 +-
tests/spec/Extend_recursive_preprocess.i | 2 +-
tests/spec/Extend_short_print.i | 4 ++--
tests/spec/add_global.i | 4 ++--
tests/spec/assigns_from_kf.i | 2 +-
tests/spec/boolean_conversion.i | 2 +-
tests/spec/bts0578.i | 4 ++--
tests/spec/bts0655.i | 4 ++--
tests/spec/comparison.i | 4 ++--
tests/spec/expr_to_term.i | 2 +-
tests/spec/extend_extern.i | 2 +-
tests/spec/heterogeneous_set_bts1146.i | 4 ++--
tests/spec/location_char.c | 4 ++--
tests/spec/logic_functions_sets.i | 2 +-
tests/spec/loop_assigns_generated.i | 2 +-
tests/spec/model.i | 4 ++--
tests/spec/pp_empty_spec.i | 4 ++--
tests/spec/property_test.i | 4 ++--
tests/spec/status_by_call_issue_890.i | 2 +-
tests/spec/type_constructors_in_env.i | 4 ++--
tests/spec/type_of_term.i | 4 ++--
tests/syntax/Refresh_visitor.i | 4 ++--
tests/syntax/add_allocates.i | 4 ++--
tests/syntax/ast_init.i | 4 ++--
tests/syntax/char_is_unsigned.i | 4 ++--
tests/syntax/clone_test.i | 4 ++--
tests/syntax/copy_visitor_bts_1073.c | 8 ++++----
tests/syntax/enum_repr.i | 8 ++++----
tests/syntax/forloophook.i | 4 ++--
tests/syntax/formals_decl_leak.i | 4 ++--
tests/syntax/get_astinfo_bts1136.i | 4 ++--
tests/syntax/ghost_parameters_formals_status.i | 4 ++--
tests/syntax/inserted_casts.c | 6 +++---
tests/syntax/logic_env.i | 4 ++--
tests/syntax/merge_loc.i | 4 ++--
tests/syntax/mutable_test.i | 7 ++-----
tests/syntax/reorder.i | 5 ++---
tests/syntax/syntactic_hook.i | 4 ++--
tests/syntax/temporary_location.c | 4 ++--
tests/syntax/transient_block.i | 4 ++--
tests/syntax/typedef_multi_1.c | 4 ++--
tests/syntax/vdescr_bts1387.i | 4 ++--
tests/syntax/visit_create_local.i | 4 ++--
tests/value/unit_tests.i | 2 +-
58 files changed, 105 insertions(+), 109 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c
index c760aa1537e..0e1c52123e2 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,7 +1,7 @@
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- MODULE: @PTEST_DIR@/name_projects.cmxs
+ MODULE: name_projects
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
*/
diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
index 5b30c58d980..d47e55b06a7 100644
--- a/tests/cil/insert_formal.i
+++ b/tests/cil/insert_formal.i
@@ -1,5 +1,5 @@
/* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
OPT: -print
*/
diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i
index ebf24f803a0..4bb64bd9e32 100644
--- a/tests/cil/mkBinOp.i
+++ b/tests/cil/mkBinOp.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -machdep x86_32 -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold
+MODULE: @PTEST_NAME@
+OPT: -machdep x86_32 -no-autoload-plugins -print -constfold
*/
int main(void) {
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c
index 959842971ac..a9778533534 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.c
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: @PTEST_NAME@
+ OPT: -eva @EVA_OPTIONS@ -deps -journal-disable
*/
int x,y,z;
diff --git a/tests/float/fval_test.i b/tests/float/fval_test.i
index f480093ba09..7cb38611d3a 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT:
*/
/* run.config*
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index dea5fdbface..71676ee94fd 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
- CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ 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
*/
diff --git a/tests/misc/behavior_names.i b/tests/misc/behavior_names.i
index 20a66a89448..63b97f6a7a2 100644
--- a/tests/misc/behavior_names.i
+++ b/tests/misc/behavior_names.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins
*/
diff --git a/tests/misc/debug_category.i b/tests/misc/debug_category.i
index 6b4a7dbc2c3..f4b77fa6c36 100644
--- a/tests/misc/debug_category.i
+++ b/tests/misc/debug_category.i
@@ -1,5 +1,5 @@
/* run.config*
-MODULE: tests/misc/Debug_category.cmxs
+MODULE: Debug_category
EXIT: 0
OPT: -test-msg-key help -test-warn-key="a=inactive"
OPT: -test-msg-key a -test-warn-key="a=inactive"
diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i
index 40748281b88..6ae8e0fd0e9 100644
--- a/tests/misc/filepath.i
+++ b/tests/misc/filepath.i
@@ -1,6 +1,6 @@
/* run.config*
- MODULE: tests/misc/filepath_test.cmxs
- COMMENT: the '-load' option below intentionally contains an error
+ MODULE: filepath_test
+ COMMENT: the '-load' option below intentionally contains an error
EXIT: 1
OPT: -no-autoload-plugins -load nonexistent_file.sav
*/
diff --git a/tests/misc/version.i b/tests/misc/version.i
index 2b739ebbd83..3691d73eeae 100644
--- a/tests/misc/version.i
+++ b/tests/misc/version.i
@@ -1,4 +1,4 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins
*/
diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c
index 7b8f05dda8a..400b9cdfb01 100644
--- a/tests/pdg/sets.c
+++ b/tests/pdg/sets.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@ -lib-entry -main f -pdg -inout "
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-lib-entry -main f -pdg -inout "
*/
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index b50076a1a38..24716e19288 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -journal-disable -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -main main2
+ MODULE: @PTEST_NAME@
+ OPT: -journal-disable -then -main main2
*/
/* bug 971: */
volatile foo;
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index acafbd74299..e8808595b16 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,5 +1,5 @@
/* run.config
-# EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+# MODULE: @PTEST_NAME@
OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva @EVA_OPTIONS@ -journal-disable
*/
diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index 85228eb7dfd..05de1247ae2 100644
--- a/tests/spec/Extend.i
+++ b/tests/spec/Extend.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 -copy -kernel-warn-key=annot-error=active
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -copy -kernel-warn-key=annot-error=active
*/
/*@ foo x == 0;
diff --git a/tests/spec/Extend_preprocess.i b/tests/spec/Extend_preprocess.i
index 24b2d061048..cf9e4d13578 100644
--- a/tests/spec/Extend_preprocess.i
+++ b/tests/spec/Extend_preprocess.i
@@ -1,5 +1,5 @@
/* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
*/
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index 319f9310fa3..ea7924d97db 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -1,5 +1,5 @@
/* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
*/
diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i
index d3f776e538a..97812f290c0 100644
--- a/tests/spec/Extend_short_print.i
+++ b/tests/spec/Extend_short_print.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
*/
/*@
diff --git a/tests/spec/add_global.i b/tests/spec/add_global.i
index 7ed406648a9..08d58179a4b 100644
--- a/tests/spec/add_global.i
+++ b/tests/spec/add_global.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
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -print
*/
int main () { return 0; }
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
index 87084d55a6f..d921cdd4e84 100644
--- a/tests/spec/assigns_from_kf.i
+++ b/tests/spec/assigns_from_kf.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT: -kernel-warn-key ghost:bad-use=inactive -print
*/
// Note: we deactivate "ghost:bad-use" because the typing phase checks on call
diff --git a/tests/spec/boolean_conversion.i b/tests/spec/boolean_conversion.i
index 1c815309a3d..78edea3a0b7 100644
--- a/tests/spec/boolean_conversion.i
+++ b/tests/spec/boolean_conversion.i
@@ -1,5 +1,5 @@
/* run.config*
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
STDOPT:
*/
void __FC_assert(int c);
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index c94e20665e6..7cdc9f445b4 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@
+ MODULE: @PTEST_NAME@
+ OPT: -print -no-autoload-plugins
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/spec/bts0655.i b/tests/spec/bts0655.i
index b5947620ab9..160d6aa62b3 100644
--- a/tests/spec/bts0655.i
+++ b/tests/spec/bts0655.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
*/
/*@
@ ensures \result == \max( a, b );
diff --git a/tests/spec/comparison.i b/tests/spec/comparison.i
index a62a8a65c77..d29dcb424b1 100644
--- a/tests/spec/comparison.i
+++ b/tests/spec/comparison.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
*/
/*@ predicate foo(boolean a, boolean b) = a == b; */
diff --git a/tests/spec/expr_to_term.i b/tests/spec/expr_to_term.i
index 88b15b296dc..97a83ecea58 100644
--- a/tests/spec/expr_to_term.i
+++ b/tests/spec/expr_to_term.i
@@ -1,5 +1,5 @@
/* run.config
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
OPT: -keep-logical-operators -print
*/
diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
index c3c61836044..a56330e2b6a 100644
--- a/tests/spec/extend_extern.i
+++ b/tests/spec/extend_extern.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT:
*/
/*@ predicate load(char * x) = \true ; */
diff --git a/tests/spec/heterogeneous_set_bts1146.i b/tests/spec/heterogeneous_set_bts1146.i
index 98c508eb2fd..bce7b3a7b2c 100644
--- a/tests/spec/heterogeneous_set_bts1146.i
+++ b/tests/spec/heterogeneous_set_bts1146.i
@@ -1,7 +1,7 @@
/* run.config
DONTRUN: bugfix in progress
- EXECNOW: make -s tests/spec/Type_of_term.cmxs
- OPT: -load-module ./tests/spec/Type_of_term.cmxs -print
+ MODULE: Type_of_term
+ OPT: -no-autoload-plugins -print
*/
/*@ lemma foo: \union(1) == \union(1.0); */
diff --git a/tests/spec/location_char.c b/tests/spec/location_char.c
index 99339a087cf..bdfc8dbeab1 100644
--- a/tests/spec/location_char.c
+++ b/tests/spec/location_char.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
*/
/*@ requires x <= 0;
diff --git a/tests/spec/logic_functions_sets.i b/tests/spec/logic_functions_sets.i
index 60190e8cc24..1ab710d70bf 100644
--- a/tests/spec/logic_functions_sets.i
+++ b/tests/spec/logic_functions_sets.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins
*/
diff --git a/tests/spec/loop_assigns_generated.i b/tests/spec/loop_assigns_generated.i
index f85c8c5a1cc..0543d690439 100644
--- a/tests/spec/loop_assigns_generated.i
+++ b/tests/spec/loop_assigns_generated.i
@@ -1,5 +1,5 @@
/* run.config*
-MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+MODULE: @PTEST_NAME@
OPT:
*/
diff --git a/tests/spec/model.i b/tests/spec/model.i
index 840ab0193bc..4faeec7d188 100644
--- a/tests/spec/model.i
+++ b/tests/spec/model.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+MODULE: @PTEST_NAME@
+STDOPT: +"-no-autoload-plugins"
*/
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 6d337f8500a..7890ba4a2f0 100644
--- a/tests/spec/pp_empty_spec.i
+++ b/tests/spec/pp_empty_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
*/
int main(void) {
int x = 0;
diff --git a/tests/spec/property_test.i b/tests/spec/property_test.i
index 6f1de940f0c..a638952ac37 100644
--- a/tests/spec/property_test.i
+++ b/tests/spec/property_test.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/spec/status_by_call_issue_890.i b/tests/spec/status_by_call_issue_890.i
index d3209b6bea9..7102449b8d3 100644
--- a/tests/spec/status_by_call_issue_890.i
+++ b/tests/spec/status_by_call_issue_890.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
*/
struct list { struct list *next; };
diff --git a/tests/spec/type_constructors_in_env.i b/tests/spec/type_constructors_in_env.i
index 636049ed329..f7525f869c8 100644
--- a/tests/spec/type_constructors_in_env.i
+++ b/tests/spec/type_constructors_in_env.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
*/
/*@ type foo = A | B; */
diff --git a/tests/spec/type_of_term.i b/tests/spec/type_of_term.i
index 81964fc9dbe..b117a9ee945 100644
--- a/tests/spec/type_of_term.i
+++ b/tests/spec/type_of_term.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s tests/spec/Type_of_term.cmxs
- OPT: -load-module tests/spec/Type_of_term.cmxs -print
+ MODULE: Type_of_term
+ STDOPT:
*/
int t [42];
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index edf44c1c372..6bf2f55e42e 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @EVA_OPTIONS@
+ MODULE: @PTEST_NAME@
+ OPT: @EVA_OPTIONS@
*/
struct S { int i; };
diff --git a/tests/syntax/add_allocates.i b/tests/syntax/add_allocates.i
index 2153e41ea67..67b339d8fed 100644
--- a/tests/syntax/add_allocates.i
+++ b/tests/syntax/add_allocates.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
+ MODULE: @PTEST_NAME@
+ STDOPT:
*/
diff --git a/tests/syntax/ast_init.i b/tests/syntax/ast_init.i
index 1e9aad67b5d..7e0d7dd7df1 100644
--- a/tests/syntax/ast_init.i
+++ b/tests/syntax/ast_init.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) { return x; }
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index a3fbe427e1e..771ea26e680 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/machdep_char_unsigned.cmxs
- OPT:-print -load-module @PTEST_DIR@/machdep_char_unsigned -machdep unsigned_char -then -constfold -rte
+ MODULE: machdep_char_unsigned
+ OPT:-print -machdep unsigned_char -then -constfold -rte
*/
char t[10];
diff --git a/tests/syntax/clone_test.i b/tests/syntax/clone_test.i
index 7d94b47b613..358db8f4602 100644
--- a/tests/syntax/clone_test.i
+++ b/tests/syntax/clone_test.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
*/
/*@
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index a20b81af83f..ec7e1ab1805 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,8 +1,8 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@_bis.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@_bis -test -then-on filtered -print
+ MODULE: @PTEST_NAME@
+ OPT:
+ MODULE: @PTEST_NAME@_bis
+ OPT: -test -then-on filtered -print
*/
#include "stdio.h"
diff --git a/tests/syntax/enum_repr.i b/tests/syntax/enum_repr.i
index 8cf7d3d4b1f..bee2bcb681f 100644
--- a/tests/syntax/enum_repr.i
+++ b/tests/syntax/enum_repr.i
@@ -1,8 +1,8 @@
/* run.config
-EXECNOW: make -s tests/syntax/Enum_repr.cmxs
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums int -print
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-short-enums -print
-OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-enums -print
+ MODULE: Enum_repr
+ OPT: -machdep x86_32 -enums int -print
+ OPT: -machdep x86_32 -enums gcc-short-enums -print
+ OPT: -machdep x86_32 -enums gcc-enums -print
*/
// is represented by | int | gcc-enums | gcc-short-enums
diff --git a/tests/syntax/forloophook.i b/tests/syntax/forloophook.i
index d9e38bd7b22..918fadf7579 100644
--- a/tests/syntax/forloophook.i
+++ b/tests/syntax/forloophook.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
*/
void f() {
for (int i=0; i< 10; i++);
diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i
index 93a7dc265a7..0b767a13285 100644
--- a/tests/syntax/formals_decl_leak.i
+++ b/tests/syntax/formals_decl_leak.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -print -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @PTEST_DIR@/@PTEST_NAME@_1.i
+ MODULE: @PTEST_NAME@
+ OPT: -print -no-autoload-plugins @PTEST_DIR@/@PTEST_NAME@_1.i
*/
void f(int x);
diff --git a/tests/syntax/get_astinfo_bts1136.i b/tests/syntax/get_astinfo_bts1136.i
index 694aacdf379..0e47cfb677f 100644
--- a/tests/syntax/get_astinfo_bts1136.i
+++ b/tests/syntax/get_astinfo_bts1136.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) { return x; }
int g (int x) { return x; }
diff --git a/tests/syntax/ghost_parameters_formals_status.i b/tests/syntax/ghost_parameters_formals_status.i
index 4698b9f77e2..b83bc5cd530 100644
--- a/tests/syntax/ghost_parameters_formals_status.i
+++ b/tests/syntax/ghost_parameters_formals_status.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: -no-autoload-plugins
*/
void declaration_void(void) /*@ ghost (int x, int y) */ ;
diff --git a/tests/syntax/inserted_casts.c b/tests/syntax/inserted_casts.c
index 805496d3d23..bd24edbeace 100644
--- a/tests/syntax/inserted_casts.c
+++ b/tests/syntax/inserted_casts.c
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
- STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" +"-machdep x86_64"
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-no-autoload-plugins"
+ STDOPT: +"-no-autoload-plugins" +"-machdep x86_64"
*/
#include "stddef.h"
int f(int b)
diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i
index 9570e109382..1f69232742a 100644
--- a/tests/syntax/logic_env.i
+++ b/tests/syntax/logic_env.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/logic_env_script.cmxs
-OPT: -load-module @PTEST_DIR@/logic_env_script
+ MODULE: logic_env_script
+ OPT: -no-autoload-plugins
*/
//@ predicate foo(integer x) = x == 0;
diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i
index 8f08173f151..2a93071ea4d 100644
--- a/tests/syntax/merge_loc.i
+++ b/tests/syntax/merge_loc.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s tests/syntax/pp_lines.cmxs
- STDOPT: #"-load-module tests/syntax/pp_lines.cmxs"
+ MODULE: pp_lines
+ STDOPT:
*/
// Test locations when cabs2cil merges declarations and tentative definitions
diff --git a/tests/syntax/mutable_test.i b/tests/syntax/mutable_test.i
index 3c480aa0534..a2c6ccc471e 100644
--- a/tests/syntax/mutable_test.i
+++ b/tests/syntax/mutable_test.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
+ MODULE: @PTEST_NAME@
+ OPT: -no-autoload-plugins -print
*/
struct R_1 {
@@ -27,6 +27,3 @@ void f()
{
x.w.v.u.t.s.r = y;
}
-
-
-
diff --git a/tests/syntax/reorder.i b/tests/syntax/reorder.i
index a6111379307..2555be87b79 100644
--- a/tests/syntax/reorder.i
+++ b/tests/syntax/reorder.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;
@@ -14,4 +14,3 @@ void f() { x++; }
//@ requires Q: \let v = Q(255); !(!v||v) ;
void g (void);
-
diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i
index 0b5e7a8bf6a..7061a2336c6 100644
--- a/tests/syntax/syntactic_hook.i
+++ b/tests/syntax/syntactic_hook.i
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
EXIT: 1
- STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+ STDOPT: +"-no-autoload-plugins"
*/
diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c
index 765e6bccede..53903fc3d13 100644
--- a/tests/syntax/temporary_location.c
+++ b/tests/syntax/temporary_location.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+ MODULE: @PTEST_NAME@
+ OPT: -print
*/
int f(void) {
diff --git a/tests/syntax/transient_block.i b/tests/syntax/transient_block.i
index bfc8874399c..ed40f930bd9 100644
--- a/tests/syntax/transient_block.i
+++ b/tests/syntax/transient_block.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -kernel-warn-key transient-block=active
+ MODULE: @PTEST_NAME@
+ OPT: -kernel-warn-key transient-block=active
*/
void f(void) { }
diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c
index 33a8d6c3537..37f3f89dbf5 100644
--- a/tests/syntax/typedef_multi_1.c
+++ b/tests/syntax/typedef_multi_1.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/typedef_multi.cmxs
- OPT: -load-module @PTEST_DIR@/typedef_multi tests/syntax/typedef_multi_2.c
+ MODULE: typedef_multi
+ OPT: -no-autoload-plugins tests/syntax/typedef_multi_2.c
*/
#include "tests/syntax/typedef_multi.h"
diff --git a/tests/syntax/vdescr_bts1387.i b/tests/syntax/vdescr_bts1387.i
index b20b1226bd2..8c041d8a3c3 100644
--- a/tests/syntax/vdescr_bts1387.i
+++ b/tests/syntax/vdescr_bts1387.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);
int g(int);
diff --git a/tests/syntax/visit_create_local.i b/tests/syntax/visit_create_local.i
index 6d9a88989bc..e49dc7c6da8 100644
--- a/tests/syntax/visit_create_local.i
+++ b/tests/syntax/visit_create_local.i
@@ -1,5 +1,5 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on bidon -print
+MODULE: @PTEST_NAME@
+OPT: -no-autoload-plugins -then-on bidon -print
*/
void main() { int x,y; x = y; }
diff --git a/tests/value/unit_tests.i b/tests/value/unit_tests.i
index f480093ba09..7cb38611d3a 100644
--- a/tests/value/unit_tests.i
+++ b/tests/value/unit_tests.i
@@ -1,5 +1,5 @@
/* run.config
- MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
OPT:
*/
/* run.config*
--
GitLab