From e436a4aace40d7f274608be90882fe315c301b20 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 21 Jan 2019 16:49:19 +0100
Subject: [PATCH] [tests] repalce some -load-script by -load-module
---
.../introduction_of_non_explicit_cast.c | 4 ++--
tests/journal/intra.i | 6 +++---
tests/misc/behavior_names.i | 3 ++-
tests/misc/bts0452.i | 4 ++--
tests/misc/bts0489.i | 3 ++-
tests/misc/bts1201.i | 6 +++---
tests/misc/bts1347.i | 4 ++--
tests/misc/bug_0209.c | 3 ++-
tests/misc/callsite.i | 3 ++-
tests/misc/change_main.i | 3 ++-
tests/misc/cli_string_multiple_map.i | 3 ++-
tests/misc/ensures.i | 3 ++-
tests/misc/find_enclosing_loop.c | 3 ++-
tests/misc/init_from_cil.i | 3 ++-
tests/misc/issue109.i | 4 ++--
tests/misc/issue_191.c | 3 ++-
tests/misc/justcopy.i | 3 ++-
tests/misc/log_twice.i | 2 +-
tests/misc/oracle/ensures.res.oracle | 2 +-
tests/misc/oracle/save_comments.res.oracle | 9 ++++++---
tests/misc/remove_status_hyps.i | 3 ++-
tests/misc/save_comments.i | 4 ++--
tests/misc/version.i | 3 ++-
tests/misc/vis_spec.i | 3 ++-
tests/misc/well_typed_alarm.i | 4 ++--
tests/pdg/dyn_dpds.c | 8 ++++----
tests/saveload/basic.i | 10 +++++-----
tests/saveload/load_one.i | 4 ++--
tests/saveload/serialized_queue.i | 3 ++-
tests/scope/bts971.c | 4 ++--
tests/spec/bts0578.i | 2 +-
tests/spec/bts0655.i | 3 ++-
tests/spec/comparison.i | 3 ++-
tests/spec/model.i | 4 ++--
tests/spec/pp_empty_spec.i | 3 ++-
tests/spec/property_test.i | 3 ++-
tests/syntax/add_allocates.i | 3 ++-
tests/syntax/clone_test.i | 3 ++-
tests/syntax/copy_visitor_bts_1073.c | 5 +++--
tests/syntax/forloophook.i | 3 ++-
tests/syntax/formals_decl_leak.i | 3 ++-
tests/syntax/get_astinfo_bts1136.i | 3 ++-
tests/syntax/reorder.i | 3 ++-
tests/syntax/syntactic_hook.i | 4 ++--
tests/syntax/vdescr_bts1387.i | 3 ++-
tests/syntax/visit_create_local.i | 3 ++-
46 files changed, 101 insertions(+), 70 deletions(-)
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c
index 2d99b7676d0..9e95b6e88db 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.c
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c
@@ -1,8 +1,8 @@
/* run.config
- OPT: -load-script tests/constant_propagation/introduction_of_non_explicit_cast.ml -eva -eva-show-progress -deps -journal-disable
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva -eva-show-progress -deps -journal-disable
*/
-
int x,y,z;
int TAB[10];
struct st { int a, b ; } s1, s2;
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index e5d5ab00342..07b7d59e05d 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: make -s tests/journal/intra.cmxs
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module ./tests/journal/intra -journal-enable -journal-name tests/journal/result/intra_journal.ml tests/journal/intra.i > /dev/null 2> /dev/null
- CMD: @frama-c@ -load-module ./tests/journal/intra
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module ./@PTEST_DIR@/@PTEST_NAME@ -journal-enable -journal-name tests/journal/result/intra_journal.ml tests/journal/intra.i > /dev/null 2> /dev/null
+ CMD: @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@
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 969831729e9..29a60449b8a 100644
--- a/tests/misc/behavior_names.i
+++ b/tests/misc/behavior_names.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/behavior_names.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/misc/bts0452.i b/tests/misc/bts0452.i
index 98005844997..9af291b3ff3 100644
--- a/tests/misc/bts0452.i
+++ b/tests/misc/bts0452.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -typecheck -load-script tests/misc/bts0452.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -typecheck -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
-
/* must emit falls-through warning. */
int f (int foo, char** args) {
switch(foo) {
diff --git a/tests/misc/bts0489.i b/tests/misc/bts0489.i
index db94a185c42..a1672f99620 100644
--- a/tests/misc/bts0489.i
+++ b/tests/misc/bts0489.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/bts0489.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
typedef unsigned char uint8_t;
diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i
index 7e59976a1ab..cbaf4a4e3d1 100644
--- a/tests/misc/bts1201.i
+++ b/tests/misc/bts1201.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -eva-verbose 2 -load-script tests/misc/bts1201.ml -print
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -eva-verbose 2 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
*/
-void main() {
- //@ assert \true;
+void main() { //@ assert \true;
}
void main2() {
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 4351b7a05c3..54f633c7bea 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/bts1347.ml -eva-show-progress -then -report
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -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 e1c584267f9..c298d86fef8 100644
--- a/tests/misc/bug_0209.c
+++ b/tests/misc/bug_0209.c
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/bug_0209.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
// Everything is done by the script
diff --git a/tests/misc/callsite.i b/tests/misc/callsite.i
index cb222eb5e95..7a703e68904 100644
--- a/tests/misc/callsite.i
+++ b/tests/misc/callsite.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/callsite.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
// 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 9239d7f51bb..c6f70943352 100644
--- a/tests/misc/change_main.i
+++ b/tests/misc/change_main.i
@@ -1,5 +1,6 @@
/* run.config*
-OPT: -eva -main f -load-script tests/misc/change_main.ml -then-on change_main -main g -eva
+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
*/
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 35a34f02c77..7269312338b 100644
--- a/tests/misc/cli_string_multiple_map.i
+++ b/tests/misc/cli_string_multiple_map.i
@@ -1,3 +1,4 @@
/* run.config
- OPT: -load-script tests/misc/cli_string_multiple_map.ml -multiple-map a:1,b:2,a:3
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -multiple-map a:1,b:2,a:3
*/
diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i
index 140bf8122f0..ae04e6fb897 100644
--- a/tests/misc/ensures.i
+++ b/tests/misc/ensures.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/ensures.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
//@ ensures *p==1;
void main(int * p){ *p = 0; }
diff --git a/tests/misc/find_enclosing_loop.c b/tests/misc/find_enclosing_loop.c
index 0a46b537168..c9ae2839edd 100644
--- a/tests/misc/find_enclosing_loop.c
+++ b/tests/misc/find_enclosing_loop.c
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/misc/find_enclosing_loop.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
void f () {
diff --git a/tests/misc/init_from_cil.i b/tests/misc/init_from_cil.i
index 276161982d2..7316c530ffd 100644
--- a/tests/misc/init_from_cil.i
+++ b/tests/misc/init_from_cil.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/init_from_cil.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int f(int x);
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index 5d51ec4b48a..51c709c227b 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva -eva-show-progress -slevel-function main:10 -load-script tests/misc/issue109.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -eva -eva-show-progress -slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
-
void main() {
int i, j = 0;
for (i=0; i<10; i++) {
diff --git a/tests/misc/issue_191.c b/tests/misc/issue_191.c
index bbba9a680d7..c298d86fef8 100644
--- a/tests/misc/issue_191.c
+++ b/tests/misc/issue_191.c
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/issue_191.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
// Everything is done by the script
diff --git a/tests/misc/justcopy.i b/tests/misc/justcopy.i
index 1045df89354..4c0e005b4ae 100644
--- a/tests/misc/justcopy.i
+++ b/tests/misc/justcopy.i
@@ -1,3 +1,4 @@
/* run.config
- OPT: -load-script tests/misc/justcopy.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index 4d912840dfc..33f9b14b6af 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -load-script tests/misc/log_twice -eva-show-progress
+ OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
*/
int* f() {
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index 7648b92dd83..7acf87d6161 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/ensures.i:4: Warning:
+[eva:alarm] tests/misc/ensures.i:5: Warning:
function main: postcondition got status invalid.
[eva] done for function main
[kernel] main: behavior default!
diff --git a/tests/misc/oracle/save_comments.res.oracle b/tests/misc/oracle/save_comments.res.oracle
index fa8ecc7b923..939609307f2 100644
--- a/tests/misc/oracle/save_comments.res.oracle
+++ b/tests/misc/oracle/save_comments.res.oracle
@@ -2,7 +2,8 @@
Printing default project first time:
/* Generated by Frama-C */
/* run.config
- OPT: -load-script tests/misc/save_comments.ml -keep-comments
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments
*/
int f(void)
{
@@ -15,7 +16,8 @@ int f(void)
Printing default project second time:
/* Generated by Frama-C */
/* run.config
- OPT: -load-script tests/misc/save_comments.ml -keep-comments
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments
*/
int f(void)
{
@@ -34,7 +36,8 @@ End of comments
Printing saved project:
/* Generated by Frama-C */
/* run.config
- OPT: -load-script tests/misc/save_comments.ml -keep-comments
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments
*/
int f(void)
{
diff --git a/tests/misc/remove_status_hyps.i b/tests/misc/remove_status_hyps.i
index 65348944a6d..7205e3be693 100644
--- a/tests/misc/remove_status_hyps.i
+++ b/tests/misc/remove_status_hyps.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/remove_status_hyps.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int main(void) {
diff --git a/tests/misc/save_comments.i b/tests/misc/save_comments.i
index 6ee3a950e34..aaf7cccdef6 100644
--- a/tests/misc/save_comments.i
+++ b/tests/misc/save_comments.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -load-script tests/misc/save_comments.ml -keep-comments
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments
*/
-
int f() {
int x = 0;
/* Hello, I'm the f function */
diff --git a/tests/misc/version.i b/tests/misc/version.i
index cd0bcd0bf86..9e559f17570 100644
--- a/tests/misc/version.i
+++ b/tests/misc/version.i
@@ -1,3 +1,4 @@
/* run.config
- OPT: -load-script tests/misc/version.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
diff --git a/tests/misc/vis_spec.i b/tests/misc/vis_spec.i
index 9515609a61d..b550116af8a 100644
--- a/tests/misc/vis_spec.i
+++ b/tests/misc/vis_spec.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/vis_spec.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
//@ assigns \nothing;
diff --git a/tests/misc/well_typed_alarm.i b/tests/misc/well_typed_alarm.i
index ec5f84df44f..236200877af 100644
--- a/tests/misc/well_typed_alarm.i
+++ b/tests/misc/well_typed_alarm.i
@@ -1,7 +1,7 @@
/* run.config*
-OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
-
int main(int c) {
int x = 0;
int y = 0;
diff --git a/tests/pdg/dyn_dpds.c b/tests/pdg/dyn_dpds.c
index 459bd5a60d7..20168cf1621 100644
--- a/tests/pdg/dyn_dpds.c
+++ b/tests/pdg/dyn_dpds.c
@@ -1,17 +1,17 @@
/* run.config
- OPT: -load-script tests/pdg/dyn_dpds.ml -eva-show-progress -deps -journal-disable -pdg-print -pdg-verbose 2
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -deps -journal-disable -pdg-print -pdg-verbose 2
*/
/*
To have a look at the dot PDG :
- bin/toplevel.byte -deps -pdg-dot pdg -eva-show-progress -fct-pdg main tests/pdg/dyn_dpds.c ;
+ bin/toplevel.byte -deps -pdg-dot pdg -eva-show-progress -fct-pdg main @PTEST_DIR@/@PTEST_NAME@.c ;
zgrviewer pdg.main.dot
- or use tests/pdg/dyn_dpds.ml to test the dynamic dependencies.
+ or use @PTEST_DIR@/@PTEST_NAME@.ml to test the dynamic dependencies.
*/
-
int G;
int main (int a, int b, int c) {
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index d091c2203be..3b6a7040f34 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,12 +1,12 @@
/* run.config
- EXECNOW: make -s ./tests/saveload/basic.cmxs
- EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module ./tests/saveload/basic -eva -out -input -deps -eva-show-progress ./tests/saveload/basic.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
- EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav ./tests/saveload/basic.i -eva -out -input -deps -eva-show-progress > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
+ EXECNOW: make -s ./@PTEST_DIR@/@PTEST_NAME@.cmxs
+ EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@ -eva -out -input -deps -eva-show-progress ./tests/saveload/basic.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
+ EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav ./@PTEST_DIR@/@PTEST_NAME@.i -eva -out -input -deps -eva-show-progress > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
OPT: -load ./tests/saveload/result/basic.sav -eva -out -input -deps -journal-disable
- CMD: @frama-c@ -load-module ./tests/saveload/basic
+ CMD: @frama-c@ -load-module ./@PTEST_DIR@/@PTEST_NAME@
OPT: -load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable -print
OPT: -load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable
- EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-script tests/saveload/status.ml -save ./tests/saveload/result/status.sav ./tests/saveload/basic.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
+ EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-script tests/saveload/status.ml -save ./tests/saveload/result/status.sav ./@PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
OPT: -load-script tests/saveload/status.ml -load ./tests/saveload/result/status.sav
OPT: -load ./tests/saveload/result/status.sav
*/
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index 2c6aa23233a..8f58edd1679 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -load-script tests/saveload/load_one.ml -eva-show-progress
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress
*/
-
int G;
int f (int x, int y) {
diff --git a/tests/saveload/serialized_queue.i b/tests/saveload/serialized_queue.i
index fe5a57bd8f7..74c44796c1a 100644
--- a/tests/saveload/serialized_queue.i
+++ b/tests/saveload/serialized_queue.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
// empty C file, we're only interested in the script itself
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index d23783b30da..b50076a1a38 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -journal-disable -load-script tests/scope/bts971.ml -then -main main2
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -journal-disable -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -main main2
*/
-
/* bug 971: */
volatile foo;
int v;
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index 4d3a94ab5ce..ec1994bfe92 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -print -load-script ./tests/spec/bts0578.ml
+ OPT: -print -load-script ./@PTEST_DIR@/@PTEST_NAME@.ml
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/spec/bts0655.i b/tests/spec/bts0655.i
index b994e76793c..da2221a66a4 100644
--- a/tests/spec/bts0655.i
+++ b/tests/spec/bts0655.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/spec/bts0655.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
/*@
@ ensures \result == \max( a, b );
diff --git a/tests/spec/comparison.i b/tests/spec/comparison.i
index 9fc56fc54cf..91f256d4f21 100644
--- a/tests/spec/comparison.i
+++ b/tests/spec/comparison.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/spec/comparison.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
/*@ predicate foo(boolean a, boolean b) = a == b; */
diff --git a/tests/spec/model.i b/tests/spec/model.i
index 0d4fe0b8b8f..64ed17aac4a 100644
--- a/tests/spec/model.i
+++ b/tests/spec/model.i
@@ -1,8 +1,8 @@
/* run.config
-STDOPT: +"-load-script tests/spec/model.ml"
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
*/
struct S { int x; int y; };
-
typedef struct S T;
/*@ model struct S { integer z }; */
diff --git a/tests/spec/pp_empty_spec.i b/tests/spec/pp_empty_spec.i
index 0835b8c2332..9dc37baea22 100644
--- a/tests/spec/pp_empty_spec.i
+++ b/tests/spec/pp_empty_spec.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int main(void) {
int x = 0;
diff --git a/tests/spec/property_test.i b/tests/spec/property_test.i
index 07866538d3b..9be52315739 100644
--- a/tests/spec/property_test.i
+++ b/tests/spec/property_test.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/spec/property_test.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int X;
diff --git a/tests/syntax/add_allocates.i b/tests/syntax/add_allocates.i
index de0ffa3fe47..1e99f19636a 100644
--- a/tests/syntax/add_allocates.i
+++ b/tests/syntax/add_allocates.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/syntax/add_allocates.ml -print
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
*/
diff --git a/tests/syntax/clone_test.i b/tests/syntax/clone_test.i
index e0a82386a6c..5300179f885 100644
--- a/tests/syntax/clone_test.i
+++ b/tests/syntax/clone_test.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
/*@
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index 1c03240bfff..bd5fafc8252 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,6 +1,7 @@
/* run.config
-OPT: -load-script tests/syntax/copy_visitor_bts_1073.ml
-OPT: -load-script tests/syntax/copy_visitor_bts_1073_bis.ml -test -then-on filtered -print
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-script @PTEST_DIR@/@PTEST_NAME@_bis.ml -test -then-on filtered -print
*/
#include "stdio.h"
diff --git a/tests/syntax/forloophook.i b/tests/syntax/forloophook.i
index 6fee07446ff..c9a3be32f74 100644
--- a/tests/syntax/forloophook.i
+++ b/tests/syntax/forloophook.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/syntax/forloophook.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
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 6a521af4ade..f7167558fe3 100644
--- a/tests/syntax/formals_decl_leak.i
+++ b/tests/syntax/formals_decl_leak.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -print -load-script tests/syntax/formals_decl_leak.ml tests/syntax/formals_decl_leak_1.i
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs tests/syntax/formals_decl_leak_1.i
*/
void f(int x);
diff --git a/tests/syntax/get_astinfo_bts1136.i b/tests/syntax/get_astinfo_bts1136.i
index bbb4f115aa3..22c2108a19a 100644
--- a/tests/syntax/get_astinfo_bts1136.i
+++ b/tests/syntax/get_astinfo_bts1136.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/syntax/get_astinfo_bts1136.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int f (int x) { return x; }
int g (int x) { return x; }
diff --git a/tests/syntax/reorder.i b/tests/syntax/reorder.i
index a754b95d776..463c6586713 100644
--- a/tests/syntax/reorder.i
+++ b/tests/syntax/reorder.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/syntax/reorder.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int x;
diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i
index e5c19d372e4..affb7ad1e3c 100644
--- a/tests/syntax/syntactic_hook.i
+++ b/tests/syntax/syntactic_hook.i
@@ -1,7 +1,7 @@
/* run.config
- STDOPT: +"-load-script tests/syntax/syntactic_hook.ml"
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
*/
-
int f(void);
int k(int *);
diff --git a/tests/syntax/vdescr_bts1387.i b/tests/syntax/vdescr_bts1387.i
index 7ef2f74b3cc..5609ab50d7e 100644
--- a/tests/syntax/vdescr_bts1387.i
+++ b/tests/syntax/vdescr_bts1387.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/syntax/vdescr_bts1387.ml
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
int f(int);
int g(int);
diff --git a/tests/syntax/visit_create_local.i b/tests/syntax/visit_create_local.i
index 68bfe516292..9bb9143fbc8 100644
--- a/tests/syntax/visit_create_local.i
+++ b/tests/syntax/visit_create_local.i
@@ -1,4 +1,5 @@
/* run.config
-OPT: -load-script tests/syntax/visit_create_local.ml -then-on bidon -print
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on bidon -print
*/
void main() { int x,y; x = y; }
--
GitLab