diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c
index 2d99b7676d0c061844695bf90822e6ed0fe5a68c..9e95b6e88db2c472e56cd47ad852b696c28e2a8b 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 e5d5ab003425ddf34ceee667dbe4ede23b9338cd..07b7d59e05d59bbd4faf62d28c0e24e6d255c004 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 969831729e947a8c410642c19d50fbd01730a3f1..29a60449b8aa1b677b2a28e2b9098db82fa59552 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 98005844997d596e37329504f7abdabeaf175f76..9af291b3ff3deb62855d7fef610f65d0d7df84ac 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 db94a185c42a8f4948e11331ceed034f854b9a1f..a1672f99620ea2317b6cbc5cb114253cf451e003 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 7e59976a1ab11f91a4cde0c78ed7630c66fa5c14..cbaf4a4e3d114ba17709f3f7fc7bfe0c6f8f5d27 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 4351b7a05c365f721926ec2916c2d8b9ba6c7e54..54f633c7beacbf0a298590ec7bd5efb20003b577 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 e1c584267f93d9cbebcfba033d9ae35f99eec16f..c298d86fef879920629bf3d60d010d1dbcc400f6 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 cb222eb5e95aa3ea93f1f110a8eb5e8b88bca06e..7a703e68904991c3d197ae672e29738b7c8e3021 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 9239d7f51bb663bc2a4d62f841a4887970a04919..c6f70943352c91f4348680131c67bb9e27329040 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 35a34f02c7751c7f8f58cc91af0f557d408f1c04..7269312338b76e5e138cc09b65b8c7fefbd60f34 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 140bf8122f031aa574e460218275fceb1fb3112b..ae04e6fb897e157311e2131e8c00117972aaa048 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 0a46b537168e8095a426f03541433800664ae563..c9ae2839eddcd72b5160b8bf4aea7b5ab939c583 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 276161982d21dae400626a206eca75b7064b3b44..7316c530ffd80aae40e08fe701581f4591cc9dab 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 5d51ec4b48a0d12becb70887d913d3b9527781cd..51c709c227b1c61c905901b787e50e87c0825216 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 bbba9a680d785fa60685908e9b32322d466639ec..c298d86fef879920629bf3d60d010d1dbcc400f6 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 1045df89354df37d9bb6936a454ceedadd769c85..4c0e005b4aef6868cb50c9bd0480902b0e551481 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 4d912840dfc75a6f69c357e731f420a3b333ed44..33f9b14b6af9429fe2f06314e5b217562ab33b52 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 7648b92dd837a79640186839b0e38b1770b249e8..7acf87d61616ae7b517495ee6013e35bbdeaf2a7 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 fa8ecc7b92399bcdf1721529af1bad62ab343057..939609307f205e0f994526ba6ebc2ea685f0989c 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 65348944a6d4a5ede92bee270d3aa2c8352a3070..7205e3be693ee4ce5c99522cce50b3253b2ed803 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 6ee3a950e34b306f68b62dc474d4a364156afafb..aaf7cccdef62fdaaaea56d6e6b5160163941eea4 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 cd0bcd0bf8696a3febda5e79680981cf9a2aed9d..9e559f17570bc4c2406f8bc67bc46eeda2844f4d 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 9515609a61d1cc5892d2bd348a2f5ffb61f4d9cd..b550116af8a6bbbc10dd2220c840e4af47185f2b 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 ec5f84df44fadd1ae56dfd540851c7dc198c0794..236200877af3a87006d77bafa01de09eef090645 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 459bd5a60d78cfeaf7100d5e608388f1caaa6a41..20168cf1621c6ed2ae366c5dc958e353dd524c74 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 d091c2203be2d30c683283c29998dddb3d416940..3b6a7040f3408157f470d4c05ade9eb9fb199eee 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 2c6aa23233a1a0d9baf17cbd8442b40a14c40e4f..8f58edd16793be9f8f058ad48543ab1df2132096 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 fe5a57bd8f72e2e63b0b2930443f942be55eecc4..74c44796c1aa09496c586db9c2ebb503fe21d6e8 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 d23783b30da5267e2f5364fa961f46bd80ee0847..b50076a1a38082a0c1f3d15ae9b1cfa66e8fa6e0 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 4d3a94ab5cecf0919d35a0beeea9433f38f410c8..ec1994bfe925546eb0abd2a6e017c834b22b6bff 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 b994e76793c1467df1e4d2dc3af4ba9bda747209..da2221a66a4de0ca1ea254a5d8ee2baba95d28bf 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 9fc56fc54cfb485abfc7007da7dfae3add8102e1..91f256d4f216f06b7c1963c0aae84b906edce1c5 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 0d4fe0b8b8f4672fb9ff0bc29b15e1669f8375c2..64ed17aac4a53c5cd70f5ecce2f46f8179556f38 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 0835b8c2332205289f637c06c42bcf7597904778..9dc37baea22c7014480743e6273892bd373ff8c9 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 07866538d3b1fcd413af495a25efa29e3c5d35c2..9be523157394897411925dd8e6aba1cd2b4b03e8 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 de0ffa3fe47e7ec04c07eda84e9e262a483a07c4..1e99f19636a1ab3e93bea31c712181307e0f0f1c 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 e0a82386a6c8f795a3e7d70252220e76f625f0e2..5300179f885c0e0b77db760d044d1019550d3de5 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 1c03240bfff694e5541238663e80381011ac77e7..bd5fafc82529eaebcf8b59565b318814197820d4 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 6fee07446ff502447a466480a7b40e3b9708cddb..c9a3be32f7416479d95eb6d7f302d96bf2f76961 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 6a521af4ade9356c5ed4431debc0970ff9d87596..f7167558fe3e482ae739ceb3a839f1d73f161e13 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 bbb4f115aa35e1323469e5de9abb7633af777c9b..22c2108a19a24ea1d8fbe72aade253ad21b91546 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 a754b95d776a02a5cbdd5bba66b7b75ab834d7be..463c6586713de8ee0992ade9408b0945accca7c8 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 e5c19d372e4d3f7ba2012a42514e35805d4e4d72..affb7ad1e3cb0e4606c4497c0e0e5ab28a4f3d76 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 7ef2f74b3ccce4b99ef88b539449c45b24854699..5609ab50d7ef88367379f8b790de4c17d2ffe2bd 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 68bfe516292bfea1bbb41bc7327aa4acaf026ad1..9bb9143fbc872ae429dad85bd603ffe9db023692 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; }