From 916bd55103de09dcea68287e92c73c6e2fc8aeab Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 23 Jan 2019 16:51:59 +0100
Subject: [PATCH] [tests] replace most remaining -load-script with -load-module
also fixes list of `.ml` files in test directories belonging to the kernel
---
Makefile | 28 +++++++++------
src/plugins/aorai/Makefile.in | 4 +--
src/plugins/aorai/tests/aorai/assigns.c | 3 +-
src/plugins/wp/tests/wp_plugin/combined.c | 3 +-
src/plugins/wp/tests/wp_plugin/combined.ml | 22 ------------
.../wp_plugin/oracle/combined.res.oracle | 36 +++++++++----------
tests/builtins/big_local_array.i | 3 +-
tests/float/fval_test.i | 4 +--
tests/journal/control.i | 6 ++--
tests/libc/fc_libc.c | 7 ++--
tests/libc/oracle/fc_libc.0.res.oracle | 6 ++--
tests/misc/custom_machdep.c | 3 +-
tests/misc/log_twice.i | 3 +-
tests/misc/oracle/log_twice.res.oracle | 20 +++++------
tests/misc/visitor_creates_func_bts_1349.i | 3 +-
...49.ml => visitor_creates_func_bts_1349.ml} | 0
tests/pdg/sets.c | 4 +--
tests/rte/precond2.c | 3 +-
tests/rte/threefunc.c | 3 +-
tests/rte/twofunc.c | 3 +-
tests/rte/twofunc3.c | 3 +-
tests/saveload/basic.i | 5 +--
tests/saveload/oracle/basic_sav.1.res | 6 ++--
tests/saveload/oracle/basic_sav.res | 6 ++--
tests/scope/zones.c | 2 +-
tests/spec/bts0578.i | 3 +-
tests/syntax/char_is_unsigned.i | 5 +--
tests/syntax/copy_visitor_bts_1073.c | 3 +-
tests/syntax/logic_env.i | 3 +-
tests/syntax/typedef_multi_1.c | 3 +-
30 files changed, 103 insertions(+), 100 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_plugin/combined.ml
rename tests/misc/{Visitor_creates_func_bts_1349.ml => visitor_creates_func_bts_1349.ml} (100%)
diff --git a/Makefile b/Makefile
index ac365806961..4e51302ae7d 100644
--- a/Makefile
+++ b/Makefile
@@ -958,6 +958,11 @@ PLUGIN_CMO:= options generator rte visit register
PLUGIN_DISTRIBUTED:=yes
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_TESTS_DIRS:=rte rte_manual
+PLUGIN_TESTS_LIB:=\
+ tests/rte/my_annotation/my_annotation.ml \
+ tests/rte/rte_api/rte_get_annot.ml \
+ tests/rte/compute_annot/compute_annot.ml \
+ tests/rte/my_annot_proxy/my_annot_proxy.ml
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
#################
@@ -1406,17 +1411,18 @@ acsl_tests: byte
$(PRINT_EXEC) acsl_tests
find doc/speclang -name \*.c -exec ./bin/toplevel.byte$(EXE) {} \; > /dev/null
-LONELY_TESTS_ML_FILES=$(wildcard $(TEST_DIRS_AS_PLUGIN:%=tests/%/*.ml))
-LONELY_TESTS_BYTE_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmo)
-LONELY_TESTS_OPT_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmx)
-LONELY_TESTS_DYN_FILES=$(LONELY_TESTS_ML_FILES:%.ml=%.cmxs)
-$(LONELY_TESTS_BYTE_FILES): BFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-$(LONELY_TESTS_OPT_FILES): OFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-$(LONELY_TESTS_DYN_FILES): OFLAGS+=$(TEST_DIRS_AS_PLUGIN:%=-I tests/%)
-.PRECIOUS: $(LONELY_TESTS_OPT_FILES) \
- $(LONELY_TESTS_DYN_FILES) \
- $(LONELY_TESTS_BYTE_FILES) \
- $(LONELY_TESTS_BYTE_FILES:%.cmo=%.cmi)
+LONELY_TESTS_ML_FILES:=\
+ $(shell find $(TEST_DIRS_AS_PLUGIN:%=tests/%) -name '*.ml')
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+ $(eval $(file:%.ml=%.cmo): BFLAGS+=-I $(dir $(file))))
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+ $(eval $(file:%.ml=%.cmx): OFLAGS+=-I $(dir $(file))))
+$(foreach file,$(LONELY_TESTS_ML_FILES),\
+ $(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file))))
+.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \
+ $(LONELY_TESTS_DYN_FILES:%.ml=%.cmxs) \
+ $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmo) \
+ $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmi)
bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml
$(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $<
diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index 5478d009fa7..423244b822a 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -80,7 +80,7 @@ PLUGIN_NO_DEFAULT_TEST:=yes
endif
PLUGIN_TESTS_DIRS:=aorai
-PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/aorai/Aorai_test.ml
+PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/aorai/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai/name_projects.ml
include $(FRAMAC_SHARE)/Makefile.dynamic
@@ -101,7 +101,7 @@ $(Aorai_DIR)/tests/test_config_prove: \
$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
$(CHMOD_RO) $@
-Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/aorai/Aorai_test.cmxs $(Aorai_DIR)/tests/aorai/Aorai_test.cmo
+Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/aorai/Aorai_test.cmxs $(Aorai_DIR)/tests/aorai/Aorai_test.cmo $(Aorai_DIR)/tests/aorai/name_projects.cmxs $(Aorai_DIR)/tests/aorai/name_projects.cmo
# Regenerating the Makefile on need
diff --git a/src/plugins/aorai/tests/aorai/assigns.c b/src/plugins/aorai/tests/aorai/assigns.c
index 7eb67e2087b..c8d63fdb9db 100644
--- a/src/plugins/aorai/tests/aorai/assigns.c
+++ b/src/plugins/aorai/tests/aorai/assigns.c
@@ -1,7 +1,8 @@
/* run.config*
+ EXECNOW: make -s @PTEST_DIR@/name_projects.cmxs
OPT: -aorai-automata tests/aorai/assigns.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata tests/aorai/assigns_det.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata tests/aorai/assigns.ya -load-script tests/aorai/name_projects.ml -aorai-test 1 -then -print
+ OPT: -aorai-automata tests/aorai/assigns.ya -load-module @PTEST_DIR@/name_projects -aorai-test 1 -then -print
*/
int X;
diff --git a/src/plugins/wp/tests/wp_plugin/combined.c b/src/plugins/wp/tests/wp_plugin/combined.c
index e698ae498d8..33a5d1e193a 100644
--- a/src/plugins/wp/tests/wp_plugin/combined.c
+++ b/src/plugins/wp/tests/wp_plugin/combined.c
@@ -3,7 +3,8 @@
*/
/* run.config_qualif
- OPT: -wp-par 1 -load-script tests/wp_plugin/combined.ml
+ EXECNOW: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -wp-par 1 -load-module @PTEST_DIR@/@PTEST_NAME@
*/
/* ZD : this should not be here such as it cannot be tested by all frama-c
diff --git a/src/plugins/wp/tests/wp_plugin/combined.ml b/src/plugins/wp/tests/wp_plugin/combined.ml
deleted file mode 100644
index 6b9da9a3107..00000000000
--- a/src/plugins/wp/tests/wp_plugin/combined.ml
+++ /dev/null
@@ -1,22 +0,0 @@
-let main () =
- Ast.compute ();
- let module OLS = Datatype.List(Datatype.String) in
- let module OKF = Datatype.Option(Kernel_function) in
- let module OP = Datatype.Option(Property) in
- Dynamic.get
- ~plugin:"Wp" "wp_compute"
- (Datatype.func3 OKF.ty OLS.ty OP.ty Datatype.unit)
- (Some
- (try Globals.Functions.find_by_name "job"
- with Not_found -> assert false))
- []
- None;
- let report =
- Dynamic.get
- ~plugin:"Report" "print" (Datatype.func Datatype.unit Datatype.unit)
- in
- report ();
- !Db.Value.compute ();
- report ()
-
-let () = Db.Main.extend main
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 299e5c4b1a5..c8a98029136 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -7,7 +7,7 @@
Function job
------------------------------------------------------------
-Goal Assertion (file tests/wp_plugin/combined.c, line 26):
+Goal Assertion (file tests/wp_plugin/combined.c, line 27):
Assume {
Type: is_sint32(A).
(* Heap *)
@@ -17,7 +17,7 @@ Prove: (50 <= A) /\ (A <= 100).
------------------------------------------------------------
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 28):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 29):
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
(* Heap *)
@@ -39,12 +39,12 @@ Prove: (-1) <= i.
------------------------------------------------------------
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 28):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 29):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 29):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 30):
Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50).
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
@@ -68,12 +68,12 @@ Prove: P_P(a[shift_sint32(t, i) <- v][shift_sint32(t, i_1)]).
------------------------------------------------------------
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 29):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 30):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 34):
+Goal Preservation of Invariant (file tests/wp_plugin/combined.c, line 35):
Let x = 1 + j.
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j) /\ is_sint32(x).
@@ -98,12 +98,12 @@ Prove: A <= x.
------------------------------------------------------------
-Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 34):
+Goal Establishment of Invariant (file tests/wp_plugin/combined.c, line 35):
Prove: true.
------------------------------------------------------------
-Goal Assertion (file tests/wp_plugin/combined.c, line 39):
+Goal Assertion (file tests/wp_plugin/combined.c, line 40):
Let a = havoc(Mint_undef_1, Mint_0, shift_sint32(t, 0), 50).
Assume {
Type: is_sint32(A) /\ is_sint32(i_1) /\ is_sint32(j).
@@ -130,36 +130,36 @@ Prove: P_P(havoc(Mint_undef_0, a, shift_sint32(t, A), 100 - A)
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (1/3):
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (2/3):
-Effect at line 32
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (2/3):
+Effect at line 33
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 30) (3/3):
-Call Result at line 32
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 31) (3/3):
+Call Result at line 33
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (1/3):
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (2/3):
-Effect at line 37
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (2/3):
+Effect at line 38
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/combined.c, line 35) (3/3):
-Call Result at line 37
+Goal Loop assigns (file tests/wp_plugin/combined.c, line 36) (3/3):
+Call Result at line 38
Let a = shift_sint32(t, j).
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j).
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index ccf98764fd0..d6e1f531814 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,6 +1,7 @@
/* run.config*
+EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
OPT: -eva-show-progress -print -journal-disable -eva -report
-OPT: -load-script tests/builtins/big_local_array_script.ml -then-on prj -print -report
+OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva
*/
diff --git a/tests/float/fval_test.i b/tests/float/fval_test.i
index 26ba3db86ad..cabb2876892 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,6 +1,6 @@
/* run.config
-# EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
*/
/* run.config*
DONTRUN:
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 03c9193098e..8a7acc8e682 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -5,10 +5,10 @@
OPT: -load-script tests/journal/result/control_journal -journal-disable
CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
OPT: -load-script tests/journal/result/control_journal_bis -calldeps -journal-disable
- EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script tests/journal/abstract_cpt.ml -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null
+ EXECNOW: make -s @PTEST_DIR@/abstract_cpt.cmxs
+ EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null
CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-script tests/journal/abstract_cpt.ml -load-script tests/journal/use_cpt.ml
-
+ OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml
*/
int x,y,c,d;
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 5b85156aea3..a153d1c9351 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -1,7 +1,10 @@
/* run.config*
- OPT: -load-script tests/libc/check_libc_naming_conventions.ml -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-script tests/libc/check_const.ml -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs
+ EXECNOW: make -s @PTEST_DIR@/check_const.cmxs
+ EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs
+ OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
- OPT: -load-script tests/libc/check_parsing_individual_headers.ml
+ OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers.ml
CMD: ./tests/libc/check_full_libc.sh
OPT:
**/
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index ffa163ed517..c1ea9b1264b 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:157: assertion got status valid.
-[eva] tests/libc/fc_libc.c:158: assertion got status valid.
-[eva] tests/libc/fc_libc.c:159: assertion got status valid.
[eva] tests/libc/fc_libc.c:160: assertion got status valid.
+[eva] tests/libc/fc_libc.c:161: assertion got status valid.
+[eva] tests/libc/fc_libc.c:162: assertion got status valid.
+[eva] tests/libc/fc_libc.c:163: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index e92b67f2a8e..f7a377dc162 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -1,5 +1,6 @@
/* run.config*
-OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-script @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.ml -machdep custom -print -then -print
+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
COMMENT: we need a -then to test double registering of a machdep
*/
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index 33f9b14b6af..e5c6f3a5f23 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
*/
int* f() {
diff --git a/tests/misc/oracle/log_twice.res.oracle b/tests/misc/oracle/log_twice.res.oracle
index 871920c55ba..30fcb6869ca 100644
--- a/tests/misc/oracle/log_twice.res.oracle
+++ b/tests/misc/oracle/log_twice.res.oracle
@@ -5,19 +5,19 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function f <- main.
- Called from tests/misc/log_twice.i:11.
+ Called from tests/misc/log_twice.i:12.
[eva] Recording results for f
[eva] Done for function f
-[eva:locals-escaping] tests/misc/log_twice.i:11: Warning:
+[eva:locals-escaping] tests/misc/log_twice.i:12: Warning:
locals {x} escaping the scope of f through \result<f>
-[eva:alarm] tests/misc/log_twice.i:12: Warning:
+[eva:alarm] tests/misc/log_twice.i:13: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
-[kernel] tests/misc/log_twice.i:12: Warning:
+[kernel] tests/misc/log_twice.i:13: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main
[eva] done for function main
-[eva] tests/misc/log_twice.i:12:
+[eva] tests/misc/log_twice.i:13:
assertion 'Eva,dangling_pointer' got final status invalid.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -25,17 +25,17 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function f <- main.
- Called from tests/misc/log_twice.i:11.
+ Called from tests/misc/log_twice.i:12.
[eva] Recording results for f
[eva] Done for function f
-[eva:locals-escaping] tests/misc/log_twice.i:11: Warning:
+[eva:locals-escaping] tests/misc/log_twice.i:12: Warning:
locals {x} escaping the scope of f through \result<f>
-[eva:alarm] tests/misc/log_twice.i:12: Warning:
+[eva:alarm] tests/misc/log_twice.i:13: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
-[kernel] tests/misc/log_twice.i:12: Warning:
+[kernel] tests/misc/log_twice.i:13: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main
[eva] done for function main
-[eva] tests/misc/log_twice.i:12:
+[eva] tests/misc/log_twice.i:13:
assertion 'Eva,dangling_pointer' got final status invalid.
diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i
index 3fc9e30144b..a03c0cd1c45 100644
--- a/tests/misc/visitor_creates_func_bts_1349.i
+++ b/tests/misc/visitor_creates_func_bts_1349.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/misc/Visitor_creates_func_bts_1349.ml -then-on test -print
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -then-on test -print
*/
int a = 10;
diff --git a/tests/misc/Visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
similarity index 100%
rename from tests/misc/Visitor_creates_func_bts_1349.ml
rename to tests/misc/visitor_creates_func_bts_1349.ml
diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c
index c0fa077572c..3efc61ce72b 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
- OPT: -eva-show-progress -load-script @PTEST_DIR@/@PTEST_NAME@.ml -lib-entry -main f -pdg -inout -journal-disable -pdg-print -pdg-verbose 2
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -eva-show-progress -load-module @PTEST_DIR@/@PTEST_NAME@ -lib-entry -main f -pdg -inout -journal-disable -pdg-print -pdg-verbose 2
*/
diff --git a/tests/rte/precond2.c b/tests/rte/precond2.c
index 2c3844e7574..72d360e0d96 100644
--- a/tests/rte/precond2.c
+++ b/tests/rte/precond2.c
@@ -1,5 +1,6 @@
/* run.config
- OPT: -warn-special-float none -load-script tests/rte/compute_annot/compute_annot.ml -journal-disable
+ EXECNOW: make -s @PTEST_DIR@/compute_annot/compute_annot.cmxs
+ OPT: -warn-special-float none -load-module @PTEST_DIR@/compute_annot/compute_annot -journal-disable
*/
int global = 15;
diff --git a/tests/rte/threefunc.c b/tests/rte/threefunc.c
index 44aa8d37cd2..6220079b7fe 100644
--- a/tests/rte/threefunc.c
+++ b/tests/rte/threefunc.c
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/rte/my_annotation/my_annotation.ml
+EXECNOW: make -s @PTEST_DIR@/my_annotation/my_annotation.cmxs
+OPT: -load-module @PTEST_DIR@/my_annotation/my_annotation.ml
*/
diff --git a/tests/rte/twofunc.c b/tests/rte/twofunc.c
index 38ce35dac65..2732ad9f1f9 100644
--- a/tests/rte/twofunc.c
+++ b/tests/rte/twofunc.c
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/rte/my_annot_proxy/my_annot_proxy.ml
+EXECNOW: make -s @PTEST_DIR@/my_annot_proxy/my_annot_proxy.cmxs
+OPT: -load-module @PTEST_DIR@/my_annot_proxy/my_annot_proxy
*/
diff --git a/tests/rte/twofunc3.c b/tests/rte/twofunc3.c
index 8894e7cbee4..b7102aaf708 100644
--- a/tests/rte/twofunc3.c
+++ b/tests/rte/twofunc3.c
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/rte/rte_api/rte_get_annot.ml -journal-disable
+ EXECNOW: make -s @PTEST_DIR@/rte_api/rte_get_annot.cmxs
+ OPT: -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
*/
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index 0a37b04868e..e0d5d8f8b74 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -6,8 +6,9 @@
CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
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 @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
+ EXECNOW: make -s @PTEST_DIR@/status.cmxs
+ EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -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-module @PTEST_DIR@/status -load ./tests/saveload/result/status.sav
OPT: -load ./tests/saveload/result/status.sav
*/
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index 985eb964675..05605960620 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -4,9 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/saveload/basic.i:18: assertion got status valid.
-[eva] tests/saveload/basic.i:19: starting to merge loop iterations
-[eva:alarm] tests/saveload/basic.i:19: Warning:
+[eva] tests/saveload/basic.i:19: assertion got status valid.
+[eva] tests/saveload/basic.i:20: starting to merge loop iterations
+[eva:alarm] tests/saveload/basic.i:20: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index 985eb964675..05605960620 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -4,9 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/saveload/basic.i:18: assertion got status valid.
-[eva] tests/saveload/basic.i:19: starting to merge loop iterations
-[eva:alarm] tests/saveload/basic.i:19: Warning:
+[eva] tests/saveload/basic.i:19: assertion got status valid.
+[eva] tests/saveload/basic.i:20: starting to merge loop iterations
+[eva:alarm] tests/saveload/basic.i:20: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index 746e8d2af98..884e57b2162 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,6 +1,6 @@
/* run.config
# EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-script @PTEST_DIR@/@PTEST_NAME@.ml -eva -eva-show-progress -journal-disable
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva -eva-show-progress -journal-disable
*/
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index ec1994bfe92..c94e20665e6 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,5 +1,6 @@
/* run.config
- OPT: -print -load-script ./@PTEST_DIR@/@PTEST_NAME@.ml
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index f87954814a8..a3fbe427e1e 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,5 +1,6 @@
-/* run.config
- OPT:-print -load-script tests/syntax/machdep_char_unsigned.ml -machdep unsigned_char -then -constfold -rte
+/* 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
*/
char t[10];
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index bd5fafc8252..a20b81af83f 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,7 +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-script @PTEST_DIR@/@PTEST_NAME@_bis.ml -test -then-on filtered -print
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@_bis -test -then-on filtered -print
*/
#include "stdio.h"
diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i
index 6d808250668..9570e109382 100644
--- a/tests/syntax/logic_env.i
+++ b/tests/syntax/logic_env.i
@@ -1,5 +1,6 @@
/* run.config
-OPT: -load-script tests/syntax/logic_env_script.ml
+EXECNOW: make -s @PTEST_DIR@/logic_env_script.cmxs
+OPT: -load-module @PTEST_DIR@/logic_env_script
*/
//@ predicate foo(integer x) = x == 0;
diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c
index fac8ea32893..33a8d6c3537 100644
--- a/tests/syntax/typedef_multi_1.c
+++ b/tests/syntax/typedef_multi_1.c
@@ -1,5 +1,6 @@
/* run.config
- OPT: -load-script tests/syntax/typedef_multi.ml tests/syntax/typedef_multi_2.c
+ EXECNOW: make -s @PTEST_DIR@/typedef_multi.cmxs
+ OPT: -load-module @PTEST_DIR@/typedef_multi tests/syntax/typedef_multi_2.c
*/
#include "tests/syntax/typedef_multi.h"
--
GitLab